Vampire-SAT---5.0.1.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : GRP583-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 : n009.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:09 AM UTC 2026

% Result   : Unsatisfiable 45.82s 7.22s
% Output   : Refutation 45.82s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   66
%            Number of leaves      :   13
% Syntax   : Number of formulae    :  358 ( 358 unt;   8 def)
%            Number of atoms       :  358 ( 357 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :    3 (   3   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    7 (   3 avg)
%            Maximal term depth    :   13 (   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   :  661 ( 661   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),double_divide(identity,identity)) = X2,
    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(f29,plain,
    ! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(double_divide(identity,identity),X0)))),double_divide(identity,identity)) = X1,
    inference(superposition,[],[f1,f6]) ).

fof(f30,plain,
    ! [X0,X1] : double_divide(double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),double_divide(X1,identity))),double_divide(identity,identity)) = X1,
    inference(superposition,[],[f1,f6]) ).

fof(f31,plain,
    ! [X2,X3,X0,X1] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1))))),double_divide(X3,X0))),double_divide(identity,identity)) = X3,
    inference(superposition,[],[f1,f1]) ).

fof(f32,plain,
    ! [X0] : double_divide(double_divide(a3,double_divide(double_divide(identity,b3),double_divide(X0,sF0))),double_divide(identity,identity)) = X0,
    inference(superposition,[],[f1,f9]) ).

fof(f33,plain,
    ! [X0] : double_divide(double_divide(sF1,double_divide(double_divide(identity,c3),double_divide(X0,sF2))),double_divide(identity,identity)) = X0,
    inference(superposition,[],[f1,f13]) ).

fof(f39,plain,
    ! [X0] : double_divide(double_divide(a3,double_divide(double_divide(identity,sF5),double_divide(X0,sF6))),double_divide(identity,identity)) = X0,
    inference(superposition,[],[f1,f21]) ).

fof(f41,plain,
    ! [X0] : double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),double_divide(identity,identity)) = X0,
    inference(superposition,[],[f1,f6]) ).

fof(f42,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)),
    inference(superposition,[],[f1,f1]) ).

fof(f46,plain,
    double_divide(identity,identity) = double_divide(double_divide(identity,double_divide(identity,identity)),double_divide(identity,identity)),
    inference(superposition,[],[f41,f6]) ).

fof(f47,plain,
    ! [X0] : double_divide(identity,double_divide(double_divide(identity,X0),identity)) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)),
    inference(superposition,[],[f1,f41]) ).

fof(f49,plain,
    double_divide(identity,identity) = double_divide(identity,double_divide(identity,identity)),
    inference(forward_demodulation,[],[f46,f6]) ).

fof(f50,plain,
    identity = double_divide(identity,identity),
    inference(forward_demodulation,[],[f49,f6]) ).

fof(f51,plain,
    ! [X0] : double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),identity) = X0,
    inference(superposition,[],[f41,f50]) ).

fof(f52,plain,
    ! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),identity) = X2,
    inference(superposition,[],[f1,f50]) ).

fof(f56,plain,
    ! [X0] : double_divide(double_divide(identity,double_divide(identity,double_divide(X0,identity))),identity) = X0,
    inference(superposition,[],[f1,f50]) ).

fof(f59,plain,
    ! [X0] : double_divide(a3,double_divide(double_divide(identity,b3),double_divide(X0,sF0))) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)),
    inference(superposition,[],[f1,f32]) ).

fof(f60,plain,
    ! [X0,X1] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(X0,sF0)))),double_divide(X1,X0))),double_divide(identity,identity)) = X1,
    inference(superposition,[],[f1,f32]) ).

fof(f61,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(X0,sF0)))),double_divide(X1,X0))),identity) = X1,
    inference(forward_demodulation,[],[f60,f50]) ).

fof(f62,plain,
    ! [X0] : double_divide(a3,double_divide(double_divide(identity,b3),double_divide(X0,sF0))) = double_divide(identity,double_divide(double_divide(identity,X0),identity)),
    inference(forward_demodulation,[],[f59,f47]) ).

fof(f66,plain,
    ! [X0] : identity = double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),X0),
    inference(superposition,[],[f6,f51]) ).

fof(f71,plain,
    ! [X0] : double_divide(sF1,double_divide(double_divide(identity,c3),double_divide(X0,sF2))) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)),
    inference(superposition,[],[f1,f33]) ).

fof(f74,plain,
    ! [X0] : double_divide(sF1,double_divide(double_divide(identity,c3),double_divide(X0,sF2))) = double_divide(identity,double_divide(double_divide(identity,X0),identity)),
    inference(forward_demodulation,[],[f71,f47]) ).

fof(f83,plain,
    ! [X0] : double_divide(double_divide(identity,X0),identity) = double_divide(identity,double_divide(X0,identity)),
    inference(superposition,[],[f51,f56]) ).

fof(f236,plain,
    ! [X0,X1] : double_divide(identity,double_divide(double_divide(identity,double_divide(X1,X0)),identity)) = double_divide(double_divide(X0,double_divide(double_divide(identity,X1),identity)),double_divide(identity,identity)),
    inference(superposition,[],[f1,f66]) ).

fof(f253,plain,
    ! [X0,X1] : double_divide(identity,double_divide(double_divide(identity,double_divide(X1,X0)),identity)) = double_divide(double_divide(X0,double_divide(double_divide(identity,X1),identity)),identity),
    inference(forward_demodulation,[],[f236,f50]) ).

fof(f270,plain,
    ! [X0,X1] : double_divide(identity,double_divide(double_divide(identity,double_divide(X1,X0)),identity)) = double_divide(double_divide(X0,double_divide(identity,double_divide(X1,identity))),identity),
    inference(forward_demodulation,[],[f253,f83]) ).

fof(f278,plain,
    ! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,identity))),identity) = double_divide(identity,double_divide(identity,double_divide(double_divide(X1,X0),identity))),
    inference(forward_demodulation,[],[f270,f83]) ).

fof(f292,plain,
    ! [X0] : double_divide(double_divide(double_divide(double_divide(identity,identity),identity),double_divide(identity,double_divide(X0,identity))),double_divide(identity,identity)) = X0,
    inference(superposition,[],[f29,f6]) ).

fof(f294,plain,
    ! [X0] : double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),identity)) = double_divide(double_divide(X0,double_divide(identity,identity)),double_divide(identity,identity)),
    inference(superposition,[],[f29,f66]) ).

fof(f296,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(double_divide(identity,identity),X1)))),
    inference(superposition,[],[f1,f29]) ).

fof(f299,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(identity,X0)),identity) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
    inference(forward_demodulation,[],[f296,f50]) ).

fof(f300,plain,
    ! [X0] : double_divide(identity,double_divide(double_divide(identity,double_divide(identity,X0)),identity)) = double_divide(double_divide(X0,identity),identity),
    inference(forward_demodulation,[],[f294,f50]) ).

fof(f302,plain,
    ! [X0] : double_divide(double_divide(double_divide(identity,identity),double_divide(identity,double_divide(X0,identity))),identity) = X0,
    inference(forward_demodulation,[],[f292,f50]) ).

fof(f304,plain,
    ! [X0,X1] : double_divide(identity,double_divide(double_divide(identity,X0),identity)) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
    inference(forward_demodulation,[],[f299,f83]) ).

fof(f305,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,X0),identity))) = double_divide(double_divide(X0,identity),identity),
    inference(forward_demodulation,[],[f300,f83]) ).

fof(f307,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(double_divide(X0,double_divide(identity,identity)),identity))) = X0,
    inference(forward_demodulation,[],[f302,f278]) ).

fof(f308,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(X0,identity))) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
    inference(forward_demodulation,[],[f304,f83]) ).

fof(f309,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(identity,double_divide(X0,identity)))) = double_divide(double_divide(X0,identity),identity),
    inference(forward_demodulation,[],[f305,f83]) ).

fof(f310,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(double_divide(X0,identity),identity))) = X0,
    inference(forward_demodulation,[],[f307,f50]) ).

fof(f365,plain,
    ! [X0] : double_divide(identity,X0) = double_divide(double_divide(double_divide(X0,identity),identity),double_divide(identity,identity)),
    inference(superposition,[],[f30,f6]) ).

fof(f371,plain,
    ! [X0] : double_divide(identity,X0) = double_divide(double_divide(double_divide(X0,identity),identity),identity),
    inference(forward_demodulation,[],[f365,f50]) ).

fof(f434,plain,
    double_divide(identity,sF2) = double_divide(double_divide(sF3,identity),identity),
    inference(superposition,[],[f371,f15]) ).

fof(f435,plain,
    double_divide(identity,sF4) = double_divide(double_divide(sF5,identity),identity),
    inference(superposition,[],[f371,f19]) ).

fof(f438,plain,
    ! [X0] : double_divide(X0,identity) = double_divide(identity,double_divide(identity,double_divide(identity,X0))),
    inference(superposition,[],[f310,f371]) ).

fof(f496,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X2)),double_divide(identity,identity)) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)))),
    inference(superposition,[],[f42,f42]) ).

fof(f503,plain,
    ! [X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),identity)) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),double_divide(identity,double_divide(double_divide(identity,double_divide(X1,X0)),identity)))),double_divide(identity,identity)),
    inference(superposition,[],[f42,f66]) ).

fof(f504,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),double_divide(identity,X1))),double_divide(identity,identity)) = double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity))),
    inference(superposition,[],[f42,f42]) ).

fof(f507,plain,
    ! [X2,X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))) = double_divide(double_divide(identity,double_divide(identity,X2)),identity),
    inference(superposition,[],[f42,f50]) ).

fof(f508,plain,
    ! [X2,X3,X0,X1,X4] : double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))) = double_divide(X3,double_divide(double_divide(identity,X4),double_divide(X2,double_divide(X4,X3)))),
    inference(superposition,[],[f42,f42]) ).

fof(f512,plain,
    ! [X0,X1] : double_divide(double_divide(double_divide(X0,double_divide(identity,X1)),double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)))),double_divide(identity,identity)) = X1,
    inference(superposition,[],[f29,f42]) ).

fof(f513,plain,
    ! [X2,X0,X1] : double_divide(double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)))),double_divide(identity,identity)) = X2,
    inference(superposition,[],[f1,f42]) ).

fof(f521,plain,
    ! [X0,X1] : double_divide(identity,X1) = double_divide(double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity))),double_divide(identity,identity)),
    inference(superposition,[],[f1,f42]) ).

fof(f523,plain,
    ! [X0,X1] : identity = double_divide(X0,double_divide(double_divide(identity,X1),double_divide(identity,double_divide(X1,X0)))),
    inference(superposition,[],[f41,f42]) ).

fof(f525,plain,
    ! [X2,X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),double_divide(double_divide(X2,double_divide(identity,identity)),double_divide(X1,X0)))) = X2,
    inference(superposition,[],[f1,f42]) ).

fof(f527,plain,
    ! [X2,X3,X0,X1] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(identity,double_divide(double_divide(identity,identity),X2))),double_divide(X3,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))))),double_divide(identity,identity)) = X3,
    inference(superposition,[],[f1,f42]) ).

fof(f528,plain,
    ! [X2,X3,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X2))),double_divide(X3,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))))),identity) = X3,
    inference(forward_demodulation,[],[f527,f50]) ).

fof(f530,plain,
    ! [X2,X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),double_divide(double_divide(X2,identity),double_divide(X1,X0)))) = X2,
    inference(forward_demodulation,[],[f525,f50]) ).

fof(f533,plain,
    ! [X0,X1] : double_divide(identity,X1) = double_divide(double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(double_divide(identity,double_divide(identity,X0)),identity)),identity),
    inference(forward_demodulation,[],[f521,f50]) ).

fof(f541,plain,
    ! [X2,X0,X1] : double_divide(double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(double_divide(identity,double_divide(identity,X0)),identity))),identity) = X2,
    inference(forward_demodulation,[],[f513,f50]) ).

fof(f542,plain,
    ! [X0,X1] : double_divide(double_divide(double_divide(X0,double_divide(identity,X1)),double_divide(identity,double_divide(double_divide(identity,double_divide(identity,X0)),identity))),identity) = X1,
    inference(forward_demodulation,[],[f512,f50]) ).

fof(f545,plain,
    ! [X2,X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))) = double_divide(identity,double_divide(double_divide(identity,X2),identity)),
    inference(forward_demodulation,[],[f507,f83]) ).

fof(f548,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),double_divide(identity,X1))),double_divide(identity,identity)) = double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(identity,double_divide(double_divide(identity,X0),identity))),
    inference(forward_demodulation,[],[f504,f47]) ).

fof(f549,plain,
    ! [X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),identity)) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X1,X0)),identity))),identity)),
    inference(forward_demodulation,[],[f503,f47]) ).

fof(f556,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X2)),double_divide(identity,identity)) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(double_divide(identity,X0),identity)))),
    inference(forward_demodulation,[],[f496,f47]) ).

fof(f592,plain,
    ! [X2,X3,X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X2))),double_divide(X3,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))))),identity)) = X3,
    inference(forward_demodulation,[],[f528,f83]) ).

fof(f596,plain,
    ! [X0,X1] : double_divide(identity,X1) = double_divide(double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(identity,double_divide(double_divide(identity,X0),identity))),identity),
    inference(forward_demodulation,[],[f533,f83]) ).

fof(f604,plain,
    ! [X2,X0,X1] : double_divide(double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(double_divide(identity,X0),identity)))),identity) = X2,
    inference(forward_demodulation,[],[f541,f83]) ).

fof(f605,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,X0)),double_divide(X0,double_divide(identity,X1))),identity))) = X1,
    inference(forward_demodulation,[],[f542,f278]) ).

fof(f607,plain,
    ! [X2,X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))) = double_divide(identity,double_divide(identity,double_divide(X2,identity))),
    inference(forward_demodulation,[],[f545,f83]) ).

fof(f610,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),double_divide(identity,X1))),double_divide(identity,identity)) = double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(identity,double_divide(identity,double_divide(X0,identity)))),
    inference(forward_demodulation,[],[f548,f83]) ).

fof(f611,plain,
    ! [X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),identity)) = double_divide(identity,double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(X1,X0)),identity),identity)))),
    inference(forward_demodulation,[],[f549,f278]) ).

fof(f618,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X2)),double_divide(identity,identity)) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(identity,double_divide(X0,identity))))),
    inference(forward_demodulation,[],[f556,f83]) ).

fof(f653,plain,
    ! [X2,X3,X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(X2,identity),double_divide(X3,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))))),identity)) = X3,
    inference(forward_demodulation,[],[f592,f438]) ).

fof(f656,plain,
    ! [X0,X1] : double_divide(identity,X1) = double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X0),double_divide(X1,double_divide(identity,X0))),identity))),
    inference(forward_demodulation,[],[f596,f278]) ).

fof(f663,plain,
    ! [X2,X0,X1] : double_divide(double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(identity,double_divide(X0,identity))))),identity) = X2,
    inference(forward_demodulation,[],[f604,f83]) ).

fof(f666,plain,
    ! [X0,X1] : double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(identity,double_divide(identity,double_divide(X0,identity)))) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,X1)),identity)),
    inference(forward_demodulation,[],[f610,f47]) ).

fof(f667,plain,
    ! [X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),identity)) = double_divide(double_divide(double_divide(double_divide(identity,double_divide(X1,X0)),identity),identity),identity),
    inference(forward_demodulation,[],[f611,f309]) ).

fof(f674,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(identity,X2),identity)) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(identity,double_divide(X0,identity))))),
    inference(forward_demodulation,[],[f618,f47]) ).

fof(f701,plain,
    ! [X2,X3] : double_divide(identity,double_divide(double_divide(double_divide(X2,identity),double_divide(X3,double_divide(identity,double_divide(identity,double_divide(X2,identity))))),identity)) = X3,
    inference(forward_demodulation,[],[f653,f607]) ).

fof(f707,plain,
    ! [X0,X1] : double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(identity,double_divide(identity,double_divide(X0,identity)))) = double_divide(identity,double_divide(identity,double_divide(double_divide(identity,X1),identity))),
    inference(forward_demodulation,[],[f666,f83]) ).

fof(f708,plain,
    ! [X0,X1] : double_divide(X0,double_divide(double_divide(identity,X1),identity)) = double_divide(identity,double_divide(identity,double_divide(X1,X0))),
    inference(forward_demodulation,[],[f667,f371]) ).

fof(f714,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(X2,identity))) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(identity,double_divide(X0,identity))))),
    inference(forward_demodulation,[],[f674,f83]) ).

fof(f737,plain,
    ! [X0,X1] : double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(identity,double_divide(identity,double_divide(X0,identity)))) = double_divide(identity,double_divide(identity,double_divide(identity,double_divide(X1,identity)))),
    inference(forward_demodulation,[],[f707,f83]) ).

fof(f738,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,double_divide(X1,identity))) = double_divide(identity,double_divide(identity,double_divide(X1,X0))),
    inference(forward_demodulation,[],[f708,f83]) ).

fof(f760,plain,
    ! [X0,X1] : double_divide(double_divide(X1,identity),identity) = double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(identity,double_divide(identity,double_divide(X0,identity)))),
    inference(forward_demodulation,[],[f737,f309]) ).

fof(f851,plain,
    ! [X2,X3,X0,X1] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(identity,double_divide(double_divide(identity,identity),double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))))),double_divide(X3,double_divide(identity,double_divide(double_divide(identity,identity),X2))))),double_divide(identity,identity)) = X3,
    inference(superposition,[],[f31,f42]) ).

fof(f864,plain,
    ! [X2,X0,X1] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)))),double_divide(X2,double_divide(identity,X1)))),double_divide(identity,identity)) = X2,
    inference(superposition,[],[f31,f42]) ).

fof(f867,plain,
    ! [X2,X3,X0,X1,X4] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X3,X4))),double_divide(X2,X1))))),double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)))),double_divide(identity,identity)) = X4,
    inference(superposition,[],[f31,f42]) ).

fof(f896,plain,
    ! [X0,X1] : c3 = double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(b3,double_divide(X1,X0))))),sF4)),double_divide(identity,identity)),
    inference(superposition,[],[f31,f17]) ).

fof(f927,plain,
    ! [X0,X1] : c3 = double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(b3,double_divide(X1,X0))))),sF4)),identity),
    inference(forward_demodulation,[],[f896,f50]) ).

fof(f956,plain,
    ! [X2,X3,X0,X1,X4] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X3,X4))),double_divide(X2,X1))))),double_divide(double_divide(identity,double_divide(identity,X0)),identity))),identity) = X4,
    inference(forward_demodulation,[],[f867,f50]) ).

fof(f959,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(double_divide(identity,double_divide(identity,X0)),identity))),double_divide(X2,double_divide(identity,X1)))),identity) = X2,
    inference(forward_demodulation,[],[f864,f50]) ).

fof(f972,plain,
    ! [X2,X3,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))))),double_divide(X3,double_divide(identity,double_divide(identity,X2))))),identity) = X3,
    inference(forward_demodulation,[],[f851,f50]) ).

fof(f1046,plain,
    ! [X0,X1] : c3 = double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(b3,double_divide(X1,X0))))),sF4),identity)),
    inference(forward_demodulation,[],[f927,f83]) ).

fof(f1074,plain,
    ! [X2,X3,X0,X1,X4] : double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X3,X4))),double_divide(X2,X1))))),double_divide(double_divide(identity,double_divide(identity,X0)),identity)),identity)) = X4,
    inference(forward_demodulation,[],[f956,f83]) ).

fof(f1077,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(double_divide(identity,double_divide(identity,X0)),identity))),double_divide(X2,double_divide(identity,X1))),identity)) = X2,
    inference(forward_demodulation,[],[f959,f83]) ).

fof(f1090,plain,
    ! [X2,X3,X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))))),double_divide(X3,double_divide(identity,double_divide(identity,X2)))),identity)) = X3,
    inference(forward_demodulation,[],[f972,f83]) ).

fof(f1159,plain,
    c3 = double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,double_divide(identity,double_divide(b3,identity)))),sF4),identity)),
    inference(forward_demodulation,[],[f1046,f607]) ).

fof(f1187,plain,
    ! [X2,X3,X0,X1,X4] : double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X3,X4))),double_divide(X2,X1))))),double_divide(identity,double_divide(double_divide(identity,X0),identity))),identity)) = X4,
    inference(forward_demodulation,[],[f1074,f83]) ).

fof(f1189,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(identity,double_divide(double_divide(identity,X0),identity)))),double_divide(X2,double_divide(identity,X1))),identity)) = X2,
    inference(forward_demodulation,[],[f1077,f83]) ).

fof(f1202,plain,
    ! [X2,X3,X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),identity),double_divide(X3,double_divide(identity,double_divide(identity,X2)))),identity)) = X3,
    inference(forward_demodulation,[],[f1090,f438]) ).

fof(f1254,plain,
    c3 = double_divide(identity,double_divide(double_divide(double_divide(double_divide(b3,identity),identity),sF4),identity)),
    inference(forward_demodulation,[],[f1159,f309]) ).

fof(f1281,plain,
    ! [X2,X3,X0,X1,X4] : double_divide(identity,double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X0),double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X3,X4))),double_divide(X2,X1)))))),identity)))) = X4,
    inference(forward_demodulation,[],[f1187,f278]) ).

fof(f1283,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,double_divide(identity,double_divide(double_divide(identity,X0),double_divide(X1,double_divide(identity,X0)))))),double_divide(X2,double_divide(identity,X1))),identity)) = X2,
    inference(forward_demodulation,[],[f1189,f738]) ).

fof(f1296,plain,
    ! [X2,X3] : double_divide(identity,double_divide(double_divide(X2,double_divide(X3,double_divide(identity,double_divide(identity,X2)))),identity)) = X3,
    inference(forward_demodulation,[],[f1202,f52]) ).

fof(f1359,plain,
    ! [X2,X3,X0,X1,X4] : double_divide(double_divide(double_divide(double_divide(identity,X0),double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X3,X4))),double_divide(X2,X1)))))),identity),identity) = X4,
    inference(forward_demodulation,[],[f1281,f309]) ).

fof(f1360,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(double_divide(double_divide(identity,X0),double_divide(X1,double_divide(identity,X0))),identity),double_divide(X2,double_divide(identity,X1))),identity)) = X2,
    inference(forward_demodulation,[],[f1283,f438]) ).

fof(f1415,plain,
    ! [X3,X0,X4] : double_divide(double_divide(double_divide(double_divide(identity,X0),double_divide(identity,double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X3,X4))),identity))))),identity),identity) = X4,
    inference(forward_demodulation,[],[f1359,f607]) ).

fof(f1447,plain,
    ! [X3,X0,X4] : double_divide(double_divide(double_divide(double_divide(identity,X0),double_divide(double_divide(double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X3,X4))),identity),identity)),identity),identity) = X4,
    inference(forward_demodulation,[],[f1415,f309]) ).

fof(f2203,plain,
    ! [X0] : identity = double_divide(X0,double_divide(double_divide(identity,double_divide(identity,double_divide(double_divide(identity,X0),identity))),double_divide(identity,identity))),
    inference(superposition,[],[f523,f66]) ).

fof(f2322,plain,
    ! [X0] : identity = double_divide(X0,double_divide(double_divide(identity,double_divide(identity,double_divide(double_divide(identity,X0),identity))),identity)),
    inference(forward_demodulation,[],[f2203,f50]) ).

fof(f2407,plain,
    ! [X0] : identity = double_divide(X0,double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X0),identity),identity)))),
    inference(forward_demodulation,[],[f2322,f278]) ).

fof(f2467,plain,
    ! [X0] : identity = double_divide(X0,double_divide(identity,X0)),
    inference(forward_demodulation,[],[f2407,f310]) ).

fof(f2551,plain,
    ! [X0] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)) = double_divide(X0,double_divide(double_divide(identity,identity),identity)),
    inference(superposition,[],[f42,f2467]) ).

fof(f2552,plain,
    ! [X0] : double_divide(double_divide(X0,double_divide(double_divide(identity,identity),identity)),double_divide(identity,identity)) = X0,
    inference(superposition,[],[f1,f2467]) ).

fof(f2599,plain,
    ! [X0] : double_divide(double_divide(X0,double_divide(identity,identity)),identity) = X0,
    inference(forward_demodulation,[],[f2552,f50]) ).

fof(f2600,plain,
    ! [X0] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)) = double_divide(X0,double_divide(identity,double_divide(identity,identity))),
    inference(forward_demodulation,[],[f2551,f83]) ).

fof(f2620,plain,
    ! [X0] : double_divide(double_divide(X0,identity),identity) = X0,
    inference(forward_demodulation,[],[f2599,f50]) ).

fof(f2621,plain,
    ! [X0] : double_divide(X0,identity) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)),
    inference(forward_demodulation,[],[f2600,f6]) ).

fof(f2632,plain,
    ! [X0] : double_divide(X0,identity) = double_divide(double_divide(identity,double_divide(identity,X0)),identity),
    inference(forward_demodulation,[],[f2621,f50]) ).

fof(f2637,plain,
    ! [X0] : double_divide(X0,identity) = double_divide(identity,double_divide(double_divide(identity,X0),identity)),
    inference(forward_demodulation,[],[f2632,f83]) ).

fof(f2639,plain,
    ! [X0] : double_divide(X0,identity) = double_divide(identity,double_divide(identity,double_divide(X0,identity))),
    inference(forward_demodulation,[],[f2637,f83]) ).

fof(f2743,plain,
    sF0 = double_divide(sF1,identity),
    inference(superposition,[],[f2620,f11]) ).

fof(f2746,plain,
    sF6 = double_divide(sF7,identity),
    inference(superposition,[],[f2620,f23]) ).

fof(f2755,plain,
    ! [X0] : double_divide(identity,double_divide(identity,X0)) = X0,
    inference(superposition,[],[f310,f2620]) ).

fof(f2759,plain,
    ! [X0] : double_divide(X0,identity) = double_divide(identity,X0),
    inference(superposition,[],[f371,f2620]) ).

fof(f2763,plain,
    sF3 = double_divide(identity,sF2),
    inference(superposition,[],[f434,f2620]) ).

fof(f2764,plain,
    sF5 = double_divide(identity,sF4),
    inference(superposition,[],[f435,f2620]) ).

fof(f2773,plain,
    ! [X0] : double_divide(identity,double_divide(X0,identity)) = double_divide(double_divide(X0,identity),identity),
    inference(superposition,[],[f371,f2620]) ).

fof(f2783,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(X1,X0))),double_divide(identity,identity)) = X1,
    inference(superposition,[],[f1,f2620]) ).

fof(f2784,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(X1,X0))),identity) = X1,
    inference(forward_demodulation,[],[f2783,f50]) ).

fof(f2788,plain,
    ! [X0] : double_divide(identity,double_divide(X0,identity)) = X0,
    inference(forward_demodulation,[],[f2773,f2620]) ).

fof(f2799,plain,
    sF6 = double_divide(identity,sF7),
    inference(forward_demodulation,[],[f2746,f2759]) ).

fof(f2802,plain,
    sF0 = double_divide(identity,sF1),
    inference(forward_demodulation,[],[f2743,f2759]) ).

fof(f2815,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(X1,X0)))) = X1,
    inference(forward_demodulation,[],[f2784,f2759]) ).

fof(f2832,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(X1,X0)) = X1,
    inference(forward_demodulation,[],[f2815,f2755]) ).

fof(f2842,plain,
    ! [X0,X1] : double_divide(X0,double_divide(X1,X0)) = X1,
    inference(forward_demodulation,[],[f2832,f2788]) ).

fof(f3916,plain,
    identity = double_divide(sF7,sF6),
    inference(superposition,[],[f2467,f2799]) ).

fof(f5314,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),double_divide(identity,X1))),double_divide(identity,identity)) = double_divide(double_divide(X1,double_divide(identity,double_divide(X0,identity))),X0),
    inference(superposition,[],[f42,f530]) ).

fof(f5321,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),double_divide(identity,X1))),double_divide(identity,identity)) = double_divide(double_divide(X1,X0),X0),
    inference(forward_demodulation,[],[f5314,f2842]) ).

fof(f5476,plain,
    ! [X0,X1] : double_divide(identity,double_divide(double_divide(identity,double_divide(identity,X1)),identity)) = double_divide(double_divide(X1,X0),X0),
    inference(forward_demodulation,[],[f5321,f47]) ).

fof(f5577,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,X1)) = double_divide(double_divide(X1,X0),X0),
    inference(forward_demodulation,[],[f5476,f2842]) ).

fof(f5651,plain,
    ! [X0,X1] : double_divide(double_divide(X1,X0),X0) = X1,
    inference(forward_demodulation,[],[f5577,f2755]) ).

fof(f6070,plain,
    sF7 = double_divide(double_divide(a3,double_divide(double_divide(identity,sF5),identity)),double_divide(identity,identity)),
    inference(superposition,[],[f39,f3916]) ).

fof(f6081,plain,
    sF7 = double_divide(double_divide(a3,double_divide(double_divide(identity,sF5),identity)),identity),
    inference(forward_demodulation,[],[f6070,f50]) ).

fof(f6087,plain,
    sF7 = double_divide(identity,double_divide(a3,double_divide(double_divide(identity,sF5),identity))),
    inference(forward_demodulation,[],[f6081,f2759]) ).

fof(f6093,plain,
    sF7 = double_divide(identity,double_divide(a3,double_divide(identity,double_divide(identity,sF5)))),
    inference(forward_demodulation,[],[f6087,f2759]) ).

fof(f6097,plain,
    sF7 = double_divide(identity,double_divide(a3,sF5)),
    inference(forward_demodulation,[],[f6093,f2755]) ).

fof(f7376,plain,
    ! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,identity))),double_divide(double_divide(identity,identity),double_divide(identity,double_divide(identity,double_divide(X0,identity))))) = X1,
    inference(superposition,[],[f530,f308]) ).

fof(f7389,plain,
    ! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,identity))),double_divide(double_divide(identity,identity),double_divide(X0,identity))) = X1,
    inference(forward_demodulation,[],[f7376,f2639]) ).

fof(f7484,plain,
    ! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,identity))),double_divide(identity,double_divide(X0,identity))) = X1,
    inference(forward_demodulation,[],[f7389,f50]) ).

fof(f7555,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(X0,double_divide(X0,double_divide(identity,double_divide(X1,identity)))))) = X1,
    inference(forward_demodulation,[],[f7484,f738]) ).

fof(f7610,plain,
    ! [X0,X1] : double_divide(X0,double_divide(X0,double_divide(identity,double_divide(X1,identity)))) = X1,
    inference(forward_demodulation,[],[f7555,f2755]) ).

fof(f7659,plain,
    ! [X0,X1] : double_divide(X0,double_divide(X0,X1)) = X1,
    inference(forward_demodulation,[],[f7610,f2842]) ).

fof(f9135,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(identity,double_divide(X0,identity)))),identity))),
    inference(superposition,[],[f605,f308]) ).

fof(f9264,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(identity,double_divide(X0,identity)))),identity),
    inference(forward_demodulation,[],[f9135,f7659]) ).

fof(f9396,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(identity,double_divide(X0,identity))))),
    inference(forward_demodulation,[],[f9264,f2759]) ).

fof(f9519,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(X0,identity))),
    inference(forward_demodulation,[],[f9396,f7659]) ).

fof(f9636,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(X1,double_divide(X0,identity))),
    inference(forward_demodulation,[],[f9519,f7659]) ).

fof(f10785,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(double_divide(double_divide(X1,identity),double_divide(double_divide(X0,identity),identity)),identity)),
    inference(superposition,[],[f1296,f760]) ).

fof(f10789,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(X0,double_divide(identity,X1)),identity))) = double_divide(double_divide(identity,double_divide(X1,identity)),double_divide(identity,double_divide(double_divide(X0,identity),identity))),
    inference(superposition,[],[f308,f760]) ).

fof(f10808,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(X0,double_divide(identity,X1)),identity))) = double_divide(identity,double_divide(identity,double_divide(double_divide(X0,identity),double_divide(identity,double_divide(X1,identity))))),
    inference(forward_demodulation,[],[f10789,f738]) ).

fof(f10811,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(X1,identity),double_divide(double_divide(X0,identity),identity)),
    inference(forward_demodulation,[],[f10785,f2842]) ).

fof(f10925,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(X0,double_divide(identity,X1)),identity))) = double_divide(double_divide(X0,identity),double_divide(identity,double_divide(X1,identity))),
    inference(forward_demodulation,[],[f10808,f7659]) ).

fof(f10928,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(X1,identity),double_divide(identity,double_divide(X0,identity))),
    inference(forward_demodulation,[],[f10811,f2759]) ).

fof(f11040,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(X0,double_divide(identity,X1)),identity))) = double_divide(identity,double_divide(identity,double_divide(X1,double_divide(X0,identity)))),
    inference(forward_demodulation,[],[f10925,f738]) ).

fof(f11043,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(identity,double_divide(X0,double_divide(X1,identity)))),
    inference(forward_demodulation,[],[f10928,f738]) ).

fof(f11146,plain,
    ! [X0,X1] : double_divide(X1,double_divide(X0,identity)) = double_divide(identity,double_divide(identity,double_divide(double_divide(X0,double_divide(identity,X1)),identity))),
    inference(forward_demodulation,[],[f11040,f7659]) ).

fof(f11149,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(X0,double_divide(X1,identity)),
    inference(forward_demodulation,[],[f11043,f7659]) ).

fof(f11242,plain,
    ! [X0,X1] : double_divide(X1,double_divide(X0,identity)) = double_divide(double_divide(X0,double_divide(identity,X1)),identity),
    inference(forward_demodulation,[],[f11146,f7659]) ).

fof(f11304,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X0,double_divide(identity,X1))) = double_divide(X1,double_divide(X0,identity)),
    inference(forward_demodulation,[],[f11242,f2759]) ).

fof(f11407,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(double_divide(identity,X0),double_divide(identity,double_divide(X0,X1))),sF0)))),identity)),identity) = X1,
    inference(superposition,[],[f61,f523]) ).

fof(f11691,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(double_divide(identity,X0),double_divide(identity,double_divide(X0,X1))),sF0)))),identity))) = X1,
    inference(forward_demodulation,[],[f11407,f2759]) ).

fof(f11838,plain,
    ! [X0,X1] : double_divide(double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(double_divide(identity,X0),double_divide(identity,double_divide(X0,X1))),sF0)))),identity) = X1,
    inference(forward_demodulation,[],[f11691,f7659]) ).

fof(f11985,plain,
    ! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(double_divide(identity,X0),double_divide(identity,double_divide(X0,X1))),sF0))))) = X1,
    inference(forward_demodulation,[],[f11838,f2759]) ).

fof(f12131,plain,
    ! [X0,X1] : double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(double_divide(identity,X0),double_divide(identity,double_divide(X0,X1))),sF0))) = X1,
    inference(forward_demodulation,[],[f11985,f7659]) ).

fof(f12273,plain,
    ! [X0,X1] : double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(identity,X0),double_divide(identity,double_divide(X0,X1)))),identity)) = X1,
    inference(forward_demodulation,[],[f12131,f62]) ).

fof(f12408,plain,
    ! [X0,X1] : double_divide(identity,double_divide(double_divide(identity,X0),double_divide(identity,double_divide(X0,X1)))) = X1,
    inference(forward_demodulation,[],[f12273,f2842]) ).

fof(f12488,plain,
    ! [X0,X1] : double_divide(double_divide(X0,X1),double_divide(double_divide(identity,X0),identity)) = X1,
    inference(forward_demodulation,[],[f12408,f11304]) ).

fof(f12546,plain,
    ! [X0,X1] : double_divide(double_divide(X0,X1),double_divide(identity,double_divide(identity,X0))) = X1,
    inference(forward_demodulation,[],[f12488,f11149]) ).

fof(f12573,plain,
    ! [X0,X1] : double_divide(double_divide(X0,X1),X0) = X1,
    inference(forward_demodulation,[],[f12546,f7659]) ).

fof(f23385,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),double_divide(X0,double_divide(X2,X1)))),double_divide(identity,identity)),
    inference(superposition,[],[f42,f5651]) ).

fof(f23388,plain,
    ! [X0,X1] : double_divide(identity,double_divide(double_divide(X1,X0),identity)) = double_divide(X0,double_divide(identity,double_divide(identity,X1))),
    inference(superposition,[],[f1296,f5651]) ).

fof(f23389,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,double_divide(identity,double_divide(X1,identity)))) = double_divide(identity,double_divide(double_divide(double_divide(X1,identity),X0),identity)),
    inference(superposition,[],[f701,f5651]) ).

fof(f23392,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X0,double_divide(identity,X1))) = double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X1),X0),identity))),
    inference(superposition,[],[f656,f5651]) ).

fof(f23455,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X0,double_divide(identity,X1))) = double_divide(double_divide(double_divide(identity,X1),X0),identity),
    inference(forward_demodulation,[],[f23392,f7659]) ).

fof(f23458,plain,
    ! [X0,X1] : double_divide(double_divide(X1,identity),X0) = double_divide(X0,double_divide(identity,double_divide(identity,double_divide(X1,identity)))),
    inference(forward_demodulation,[],[f23389,f2842]) ).

fof(f23459,plain,
    ! [X0,X1] : double_divide(X0,X1) = double_divide(identity,double_divide(double_divide(X1,X0),identity)),
    inference(forward_demodulation,[],[f23388,f7659]) ).

fof(f23462,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(X2,X1))),identity)),
    inference(forward_demodulation,[],[f23385,f47]) ).

fof(f23622,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X0,double_divide(identity,X1))) = double_divide(identity,double_divide(double_divide(identity,X1),X0)),
    inference(forward_demodulation,[],[f23455,f2759]) ).

fof(f23625,plain,
    ! [X0,X1] : double_divide(X0,double_divide(X1,identity)) = double_divide(double_divide(X1,identity),X0),
    inference(forward_demodulation,[],[f23458,f7659]) ).

fof(f23626,plain,
    ! [X0,X1] : double_divide(X1,X0) = double_divide(X0,X1),
    inference(forward_demodulation,[],[f23459,f2842]) ).

fof(f23629,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(identity,double_divide(X0,double_divide(X2,X1))),
    inference(forward_demodulation,[],[f23462,f2842]) ).

fof(f23749,plain,
    ! [X0,X1] : double_divide(X1,double_divide(X0,identity)) = double_divide(identity,double_divide(double_divide(identity,X1),X0)),
    inference(forward_demodulation,[],[f23622,f11304]) ).

fof(f27100,plain,
    double_divide(identity,c3) = double_divide(double_divide(double_divide(double_divide(b3,identity),identity),sF4),identity),
    inference(superposition,[],[f7659,f1254]) ).

fof(f27573,plain,
    double_divide(identity,c3) = double_divide(identity,double_divide(double_divide(double_divide(b3,identity),identity),sF4)),
    inference(forward_demodulation,[],[f27100,f2759]) ).

fof(f27741,plain,
    double_divide(identity,c3) = double_divide(identity,double_divide(sF4,double_divide(double_divide(b3,identity),identity))),
    inference(forward_demodulation,[],[f27573,f23626]) ).

fof(f27876,plain,
    double_divide(identity,c3) = double_divide(double_divide(b3,identity),double_divide(identity,sF4)),
    inference(forward_demodulation,[],[f27741,f9636]) ).

fof(f27964,plain,
    double_divide(identity,c3) = double_divide(double_divide(identity,sF4),double_divide(b3,identity)),
    inference(forward_demodulation,[],[f27876,f23626]) ).

fof(f28025,plain,
    double_divide(identity,c3) = double_divide(double_divide(identity,sF4),double_divide(identity,b3)),
    inference(forward_demodulation,[],[f27964,f11149]) ).

fof(f28059,plain,
    double_divide(identity,c3) = double_divide(double_divide(identity,b3),double_divide(identity,sF4)),
    inference(forward_demodulation,[],[f28025,f23626]) ).

fof(f28073,plain,
    double_divide(identity,c3) = double_divide(double_divide(identity,b3),sF5),
    inference(forward_demodulation,[],[f28059,f2764]) ).

fof(f28084,plain,
    double_divide(identity,c3) = double_divide(sF5,double_divide(identity,b3)),
    inference(forward_demodulation,[],[f28073,f23626]) ).

fof(f33171,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),double_divide(double_divide(X2,X1),X0))),double_divide(identity,identity)),
    inference(superposition,[],[f42,f12573]) ).

fof(f33248,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(double_divide(identity,identity),double_divide(identity,double_divide(double_divide(identity,identity),double_divide(double_divide(X2,X1),X0)))),
    inference(forward_demodulation,[],[f33171,f23625]) ).

fof(f33429,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(double_divide(identity,identity),double_divide(identity,double_divide(double_divide(double_divide(X2,X1),X0),identity))),
    inference(forward_demodulation,[],[f33248,f23749]) ).

fof(f33572,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(X2,X1),X0),double_divide(identity,identity)))),
    inference(forward_demodulation,[],[f33429,f738]) ).

fof(f33683,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(double_divide(double_divide(X2,X1),X0),double_divide(identity,identity)),
    inference(forward_demodulation,[],[f33572,f7659]) ).

fof(f33765,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(double_divide(identity,identity),double_divide(double_divide(X2,X1),X0)),
    inference(forward_demodulation,[],[f33683,f23625]) ).

fof(f33811,plain,
    ! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(identity,X2),X0)) = double_divide(identity,double_divide(double_divide(X2,X1),X0)),
    inference(forward_demodulation,[],[f33765,f50]) ).

fof(f36706,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X2)),double_divide(identity,identity)) = double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X0,X1)))),
    inference(superposition,[],[f42,f23626]) ).

fof(f37249,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,identity),double_divide(identity,double_divide(double_divide(identity,identity),X2))) = double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X0,X1)))),
    inference(forward_demodulation,[],[f36706,f23625]) ).

fof(f37809,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,identity),double_divide(identity,double_divide(X2,identity))) = double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X0,X1)))),
    inference(forward_demodulation,[],[f37249,f23749]) ).

fof(f38286,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(X2,double_divide(identity,identity)))) = double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X0,X1)))),
    inference(forward_demodulation,[],[f37809,f738]) ).

fof(f38643,plain,
    ! [X2,X0,X1] : double_divide(X2,double_divide(identity,identity)) = double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X0,X1)))),
    inference(forward_demodulation,[],[f38286,f7659]) ).

fof(f38905,plain,
    ! [X2,X0,X1] : double_divide(X2,identity) = double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X0,X1)))),
    inference(forward_demodulation,[],[f38643,f50]) ).

fof(f53111,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X1))),double_divide(identity,double_divide(identity,double_divide(X0,identity))))),identity),
    inference(superposition,[],[f663,f523]) ).

fof(f53114,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(double_divide(identity,double_divide(identity,double_divide(X0,identity))),double_divide(double_divide(identity,double_divide(identity,identity)),double_divide(identity,double_divide(identity,double_divide(X1,identity))))),identity),
    inference(superposition,[],[f663,f308]) ).

fof(f53183,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),double_divide(double_divide(identity,double_divide(identity,double_divide(identity,c3))),double_divide(identity,double_divide(identity,double_divide(sF1,identity))))),identity),
    inference(superposition,[],[f663,f74]) ).

fof(f53598,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),double_divide(double_divide(identity,double_divide(identity,double_divide(identity,c3))),double_divide(identity,double_divide(identity,double_divide(sF1,identity)))))),
    inference(forward_demodulation,[],[f53183,f2759]) ).

fof(f53667,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(X0,identity))),double_divide(double_divide(identity,double_divide(identity,identity)),double_divide(identity,double_divide(identity,double_divide(X1,identity)))))),
    inference(forward_demodulation,[],[f53114,f2759]) ).

fof(f53670,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X1))),double_divide(identity,double_divide(identity,double_divide(X0,identity)))))),
    inference(forward_demodulation,[],[f53111,f2759]) ).

fof(f54028,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(double_divide(identity,X0),identity),double_divide(double_divide(double_divide(identity,double_divide(identity,double_divide(identity,c3))),double_divide(identity,double_divide(identity,double_divide(sF1,identity)))),identity)),
    inference(forward_demodulation,[],[f53598,f23749]) ).

fof(f54097,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(double_divide(double_divide(identity,double_divide(identity,identity)),double_divide(identity,double_divide(identity,double_divide(X1,identity)))),identity)),
    inference(forward_demodulation,[],[f53667,f23749]) ).

fof(f54100,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X1))),double_divide(identity,double_divide(identity,double_divide(X0,identity)))),
    inference(forward_demodulation,[],[f53670,f7659]) ).

fof(f54449,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(double_divide(identity,X0),identity),double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,c3))),double_divide(identity,double_divide(identity,double_divide(sF1,identity)))))),
    inference(forward_demodulation,[],[f54028,f11149]) ).

fof(f54518,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(identity,double_divide(double_divide(identity,double_divide(identity,identity)),double_divide(identity,double_divide(identity,double_divide(X1,identity)))))),
    inference(forward_demodulation,[],[f54097,f11149]) ).

fof(f54520,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X1))),double_divide(X0,identity)),
    inference(forward_demodulation,[],[f54100,f7659]) ).

fof(f54849,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(double_divide(identity,X0),identity),double_divide(double_divide(identity,double_divide(identity,c3)),double_divide(double_divide(identity,double_divide(identity,double_divide(sF1,identity))),identity))),
    inference(forward_demodulation,[],[f54449,f23749]) ).

fof(f54918,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(identity,double_divide(X1,identity))),identity))),
    inference(forward_demodulation,[],[f54518,f23749]) ).

fof(f54920,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(identity,X1),double_divide(X0,identity)),
    inference(forward_demodulation,[],[f54520,f7659]) ).

fof(f55224,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,double_divide(sF1,identity))),identity),double_divide(double_divide(identity,c3),double_divide(double_divide(identity,X0),identity)))),
    inference(forward_demodulation,[],[f54849,f23629]) ).

fof(f55290,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,double_divide(X1,identity))),identity),double_divide(identity,double_divide(identity,double_divide(X0,identity))))),
    inference(forward_demodulation,[],[f54918,f23629]) ).

fof(f55552,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,double_divide(sF1,identity)))),double_divide(double_divide(identity,c3),double_divide(double_divide(identity,X0),identity)))),
    inference(forward_demodulation,[],[f55224,f33811]) ).

fof(f55614,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,double_divide(X1,identity)))),double_divide(identity,double_divide(identity,double_divide(X0,identity))))),
    inference(forward_demodulation,[],[f55290,f33811]) ).

fof(f55848,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(identity,double_divide(identity,double_divide(sF1,identity))),double_divide(double_divide(double_divide(identity,c3),double_divide(double_divide(identity,X0),identity)),identity)),
    inference(forward_demodulation,[],[f55552,f23749]) ).

fof(f55906,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(identity,double_divide(identity,double_divide(X1,identity))),double_divide(double_divide(identity,double_divide(identity,double_divide(X0,identity))),identity)),
    inference(forward_demodulation,[],[f55614,f23749]) ).

fof(f56111,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(identity,double_divide(identity,double_divide(sF1,identity))),double_divide(identity,double_divide(double_divide(identity,c3),double_divide(double_divide(identity,X0),identity)))),
    inference(forward_demodulation,[],[f55848,f11149]) ).

fof(f56166,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(identity,double_divide(identity,double_divide(X1,identity)))))),
    inference(forward_demodulation,[],[f55906,f23629]) ).

fof(f56331,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(identity,double_divide(identity,double_divide(sF1,identity))),double_divide(c3,double_divide(double_divide(double_divide(identity,X0),identity),identity))),
    inference(forward_demodulation,[],[f56111,f23749]) ).

fof(f56384,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(identity,double_divide(identity,double_divide(X1,identity)))),
    inference(forward_demodulation,[],[f56166,f7659]) ).

fof(f56519,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(identity,double_divide(identity,double_divide(sF1,identity))),double_divide(c3,double_divide(identity,double_divide(double_divide(identity,X0),identity)))),
    inference(forward_demodulation,[],[f56331,f11149]) ).

fof(f56564,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(X1,identity)),
    inference(forward_demodulation,[],[f56384,f7659]) ).

fof(f56666,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(identity,double_divide(identity,double_divide(sF1,identity))),double_divide(identity,double_divide(identity,double_divide(double_divide(identity,X0),c3)))),
    inference(forward_demodulation,[],[f56519,f738]) ).

fof(f56701,plain,
    ! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(double_divide(X0,identity),X1)),
    inference(forward_demodulation,[],[f56564,f54920]) ).

fof(f56756,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(double_divide(identity,double_divide(identity,double_divide(sF1,identity))),double_divide(double_divide(identity,X0),c3)),
    inference(forward_demodulation,[],[f56666,f7659]) ).

fof(f56820,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(identity,double_divide(c3,double_divide(X0,double_divide(identity,double_divide(identity,double_divide(sF1,identity)))))),
    inference(forward_demodulation,[],[f56756,f23629]) ).

fof(f56862,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(identity,double_divide(c3,double_divide(X0,double_divide(sF1,identity)))),
    inference(forward_demodulation,[],[f56820,f7659]) ).

fof(f56888,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(identity,double_divide(c3,double_divide(X0,double_divide(identity,sF1)))),
    inference(forward_demodulation,[],[f56862,f11149]) ).

fof(f56905,plain,
    ! [X0] : double_divide(X0,sF2) = double_divide(identity,double_divide(c3,double_divide(X0,sF0))),
    inference(forward_demodulation,[],[f56888,f2802]) ).

fof(f58566,plain,
    ! [X2,X0,X1] : double_divide(X0,double_divide(identity,X2)) = double_divide(identity,double_divide(double_divide(double_divide(double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,X1))),identity),X0),identity)),
    inference(superposition,[],[f1360,f5651]) ).

fof(f58567,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,X2),X0) = double_divide(identity,double_divide(double_divide(double_divide(double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,X1))),identity),X0),identity)),
    inference(superposition,[],[f1360,f12573]) ).

fof(f58782,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,X2),X0) = double_divide(double_divide(double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,X1))),identity),X0),
    inference(forward_demodulation,[],[f58567,f2842]) ).

fof(f58783,plain,
    ! [X2,X0,X1] : double_divide(X0,double_divide(identity,X2)) = double_divide(double_divide(double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,X1))),identity),X0),
    inference(forward_demodulation,[],[f58566,f2842]) ).

fof(f59059,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,X2),X0) = double_divide(double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,X1)))),X0),
    inference(forward_demodulation,[],[f58782,f2759]) ).

fof(f59060,plain,
    ! [X2,X0,X1] : double_divide(X0,double_divide(identity,X2)) = double_divide(double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,X1)))),X0),
    inference(forward_demodulation,[],[f58783,f2759]) ).

fof(f59331,plain,
    ! [X2,X0] : double_divide(double_divide(X2,identity),X0) = double_divide(double_divide(identity,X2),X0),
    inference(forward_demodulation,[],[f59059,f38905]) ).

fof(f59332,plain,
    ! [X2,X0] : double_divide(double_divide(X2,identity),X0) = double_divide(X0,double_divide(identity,X2)),
    inference(forward_demodulation,[],[f59060,f38905]) ).

fof(f60921,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(double_divide(double_divide(identity,X0),double_divide(double_divide(double_divide(double_divide(identity,double_divide(identity,X1)),identity),identity),identity)),identity),identity),
    inference(superposition,[],[f1447,f523]) ).

fof(f60922,plain,
    ! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(X2,X1)) = double_divide(double_divide(double_divide(double_divide(identity,X1),double_divide(double_divide(double_divide(double_divide(identity,double_divide(identity,X2)),X0),identity),identity)),identity),identity),
    inference(superposition,[],[f1447,f530]) ).

fof(f61250,plain,
    ! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(X2,X1)) = double_divide(identity,double_divide(double_divide(double_divide(identity,X1),double_divide(double_divide(double_divide(double_divide(identity,double_divide(identity,X2)),X0),identity),identity)),identity)),
    inference(forward_demodulation,[],[f60922,f2759]) ).

fof(f61251,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(identity,double_divide(double_divide(double_divide(identity,X0),double_divide(double_divide(double_divide(double_divide(identity,double_divide(identity,X1)),identity),identity),identity)),identity)),
    inference(forward_demodulation,[],[f60921,f2759]) ).

fof(f61686,plain,
    ! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(X2,X1)) = double_divide(double_divide(identity,X1),double_divide(double_divide(double_divide(double_divide(identity,double_divide(identity,X2)),X0),identity),identity)),
    inference(forward_demodulation,[],[f61250,f2842]) ).

fof(f61687,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(identity,X0),double_divide(double_divide(double_divide(double_divide(identity,double_divide(identity,X1)),identity),identity),identity)),
    inference(forward_demodulation,[],[f61251,f2842]) ).

fof(f62118,plain,
    ! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(X2,X1)) = double_divide(double_divide(identity,X1),double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,X2)),X0),identity))),
    inference(forward_demodulation,[],[f61686,f11149]) ).

fof(f62119,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(identity,X0),double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,X1)),identity),identity))),
    inference(forward_demodulation,[],[f61687,f11149]) ).

fof(f62545,plain,
    ! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(X2,X1)) = double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,X2)),X0),double_divide(identity,X1)))),
    inference(forward_demodulation,[],[f62118,f738]) ).

fof(f62546,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,X1)),identity),double_divide(identity,X0)))),
    inference(forward_demodulation,[],[f62119,f738]) ).

fof(f62962,plain,
    ! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(X2,X1)) = double_divide(double_divide(double_divide(identity,double_divide(identity,X2)),X0),double_divide(identity,X1)),
    inference(forward_demodulation,[],[f62545,f7659]) ).

fof(f62963,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(double_divide(identity,double_divide(identity,X1)),identity),double_divide(identity,X0)),
    inference(forward_demodulation,[],[f62546,f7659]) ).

fof(f63374,plain,
    ! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(X2,X1)) = double_divide(double_divide(X2,X0),double_divide(identity,X1)),
    inference(forward_demodulation,[],[f62962,f7659]) ).

fof(f63375,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X1))),double_divide(identity,X0)),
    inference(forward_demodulation,[],[f62963,f59331]) ).

fof(f63774,plain,
    ! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(identity,X1),double_divide(identity,X0)),
    inference(forward_demodulation,[],[f63375,f7659]) ).

fof(f78940,plain,
    ! [X2,X3,X0,X1,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(double_divide(X5,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))),double_divide(double_divide(identity,double_divide(identity,X4)),double_divide(identity,double_divide(identity,double_divide(X5,identity))))),
    inference(superposition,[],[f714,f508]) ).

fof(f78945,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(double_divide(X2,double_divide(identity,double_divide(identity,double_divide(X0,identity)))),double_divide(double_divide(identity,double_divide(identity,X1)),double_divide(identity,double_divide(identity,double_divide(X2,identity))))),
    inference(superposition,[],[f714,f308]) ).

fof(f79843,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(X2,identity))),double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,double_divide(identity,double_divide(X0,identity))))))),
    inference(forward_demodulation,[],[f78945,f23629]) ).

fof(f79848,plain,
    ! [X2,X3,X0,X1,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(X5,identity))),double_divide(double_divide(identity,X4),double_divide(X5,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))))))),
    inference(forward_demodulation,[],[f78940,f23629]) ).

fof(f80296,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(double_divide(identity,double_divide(X2,identity)),double_divide(double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,double_divide(identity,double_divide(X0,identity))))),identity)),
    inference(forward_demodulation,[],[f79843,f23749]) ).

fof(f80301,plain,
    ! [X2,X3,X0,X1,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(double_divide(identity,double_divide(X5,identity)),double_divide(double_divide(double_divide(identity,X4),double_divide(X5,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))))),identity)),
    inference(forward_demodulation,[],[f79848,f23749]) ).

fof(f80745,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(double_divide(identity,double_divide(X2,identity)),double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,double_divide(identity,double_divide(X0,identity))))))),
    inference(forward_demodulation,[],[f80296,f11149]) ).

fof(f80749,plain,
    ! [X2,X3,X0,X1,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(double_divide(identity,double_divide(X5,identity)),double_divide(identity,double_divide(double_divide(identity,X4),double_divide(X5,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))))))),
    inference(forward_demodulation,[],[f80301,f11149]) ).

fof(f81184,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(identity,double_divide(double_divide(X2,identity),double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,double_divide(identity,double_divide(X0,identity))))))),
    inference(forward_demodulation,[],[f80745,f63774]) ).

fof(f81188,plain,
    ! [X2,X3,X0,X1,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(identity,double_divide(double_divide(X5,identity),double_divide(double_divide(identity,X4),double_divide(X5,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))))))),
    inference(forward_demodulation,[],[f80749,f63774]) ).

fof(f81602,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(X2,double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(identity,double_divide(identity,double_divide(X0,identity))))))),
    inference(forward_demodulation,[],[f81184,f56701]) ).

fof(f81606,plain,
    ! [X2,X3,X0,X1,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(X5,double_divide(identity,double_divide(double_divide(identity,X4),double_divide(X5,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))))))),
    inference(forward_demodulation,[],[f81188,f56701]) ).

fof(f81994,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(X2,double_divide(X1,double_divide(double_divide(X2,double_divide(identity,double_divide(identity,double_divide(X0,identity)))),identity))),
    inference(forward_demodulation,[],[f81602,f23749]) ).

fof(f81998,plain,
    ! [X2,X3,X0,X1,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(X5,double_divide(X4,double_divide(double_divide(X5,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))),identity))),
    inference(forward_demodulation,[],[f81606,f23749]) ).

fof(f82352,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(X2,double_divide(X1,double_divide(identity,double_divide(X2,double_divide(identity,double_divide(identity,double_divide(X0,identity))))))),
    inference(forward_demodulation,[],[f81994,f11149]) ).

fof(f82356,plain,
    ! [X2,X3,X0,X1,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(X5,double_divide(X4,double_divide(identity,double_divide(X5,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))))))),
    inference(forward_demodulation,[],[f81998,f11149]) ).

fof(f82632,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(X2,double_divide(X1,double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(X2,identity)))),
    inference(forward_demodulation,[],[f82352,f11304]) ).

fof(f82636,plain,
    ! [X2,X3,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(X5,double_divide(X4,double_divide(identity,double_divide(X5,double_divide(identity,double_divide(identity,double_divide(X2,identity))))))),
    inference(forward_demodulation,[],[f82356,f607]) ).

fof(f82887,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(X2,double_divide(X1,double_divide(identity,double_divide(double_divide(X0,identity),X2)))),
    inference(forward_demodulation,[],[f82632,f54920]) ).

fof(f82890,plain,
    ! [X2,X3,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(X5,double_divide(X4,double_divide(double_divide(identity,double_divide(X2,identity)),double_divide(X5,identity)))),
    inference(forward_demodulation,[],[f82636,f11304]) ).

fof(f83108,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity))) = double_divide(X2,double_divide(X1,double_divide(X0,double_divide(identity,X2)))),
    inference(forward_demodulation,[],[f82887,f56701]) ).

fof(f83111,plain,
    ! [X2,X3,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(X5,double_divide(X4,double_divide(identity,double_divide(double_divide(X2,identity),X5)))),
    inference(forward_demodulation,[],[f82890,f54920]) ).

fof(f83307,plain,
    ! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X0,double_divide(identity,X1))),identity) = double_divide(X2,double_divide(X1,double_divide(X0,double_divide(identity,X2)))),
    inference(forward_demodulation,[],[f83108,f7659]) ).

fof(f83310,plain,
    ! [X2,X3,X4,X5] : double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity))) = double_divide(X5,double_divide(X4,double_divide(X2,double_divide(identity,X5)))),
    inference(forward_demodulation,[],[f83111,f56701]) ).

fof(f83484,plain,
    ! [X2,X0,X1] : double_divide(identity,double_divide(identity,double_divide(X0,double_divide(identity,X1)))) = double_divide(X2,double_divide(X1,double_divide(X0,double_divide(identity,X2)))),
    inference(forward_demodulation,[],[f83307,f2759]) ).

fof(f83487,plain,
    ! [X2,X3,X4,X5] : double_divide(double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4))),identity) = double_divide(X5,double_divide(X4,double_divide(X2,double_divide(identity,X5)))),
    inference(forward_demodulation,[],[f83310,f7659]) ).

fof(f83621,plain,
    ! [X2,X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(X2,double_divide(X1,double_divide(X0,double_divide(identity,X2)))),
    inference(forward_demodulation,[],[f83484,f7659]) ).

fof(f83624,plain,
    ! [X2,X3,X4,X5] : double_divide(identity,double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4)))) = double_divide(X5,double_divide(X4,double_divide(X2,double_divide(identity,X5)))),
    inference(forward_demodulation,[],[f83487,f2759]) ).

fof(f83715,plain,
    ! [X2,X3,X4] : double_divide(identity,double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X4)))) = double_divide(X2,double_divide(identity,X4)),
    inference(forward_demodulation,[],[f83624,f83621]) ).

fof(f83777,plain,
    ! [X2,X3,X4] : double_divide(X3,double_divide(double_divide(X2,double_divide(X3,X4)),identity)) = double_divide(X2,double_divide(identity,X4)),
    inference(forward_demodulation,[],[f83715,f23749]) ).

fof(f83818,plain,
    ! [X2,X3,X4] : double_divide(X3,double_divide(identity,double_divide(X2,double_divide(X3,X4)))) = double_divide(X2,double_divide(identity,X4)),
    inference(forward_demodulation,[],[f83777,f11149]) ).

fof(f119549,plain,
    sF5 = double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(identity,b3),sF0)))),double_divide(identity,c3))),identity),
    inference(superposition,[],[f61,f28084]) ).

fof(f119607,plain,
    sF5 = double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(identity,b3),sF0)))),double_divide(identity,c3)))),
    inference(forward_demodulation,[],[f119549,f2759]) ).

fof(f119658,plain,
    sF5 = double_divide(double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(identity,b3),sF0)))),double_divide(identity,c3)),
    inference(forward_demodulation,[],[f119607,f7659]) ).

fof(f119708,plain,
    sF5 = double_divide(double_divide(c3,identity),double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(identity,b3),sF0))))),
    inference(forward_demodulation,[],[f119658,f59332]) ).

fof(f119756,plain,
    sF5 = double_divide(double_divide(identity,c3),double_divide(identity,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(identity,b3),sF0))))),
    inference(forward_demodulation,[],[f119708,f63374]) ).

fof(f119803,plain,
    sF5 = double_divide(identity,double_divide(c3,double_divide(a3,double_divide(double_divide(identity,b3),double_divide(double_divide(identity,b3),sF0))))),
    inference(forward_demodulation,[],[f119756,f63774]) ).

fof(f119849,plain,
    sF5 = double_divide(identity,double_divide(c3,double_divide(identity,double_divide(double_divide(double_divide(identity,b3),sF0),double_divide(b3,a3))))),
    inference(forward_demodulation,[],[f119803,f23629]) ).

fof(f119889,plain,
    sF5 = double_divide(double_divide(double_divide(double_divide(identity,b3),sF0),double_divide(b3,a3)),double_divide(c3,identity)),
    inference(forward_demodulation,[],[f119849,f11304]) ).

fof(f119926,plain,
    sF5 = double_divide(double_divide(double_divide(double_divide(identity,b3),sF0),double_divide(b3,a3)),double_divide(identity,c3)),
    inference(forward_demodulation,[],[f119889,f11149]) ).

fof(f119960,plain,
    sF5 = double_divide(double_divide(c3,identity),double_divide(double_divide(double_divide(identity,b3),sF0),double_divide(b3,a3))),
    inference(forward_demodulation,[],[f119926,f59332]) ).

fof(f119991,plain,
    sF5 = double_divide(double_divide(identity,c3),double_divide(double_divide(double_divide(identity,b3),sF0),double_divide(b3,a3))),
    inference(forward_demodulation,[],[f119960,f59331]) ).

fof(f120020,plain,
    sF5 = double_divide(double_divide(identity,c3),double_divide(double_divide(b3,a3),double_divide(double_divide(identity,b3),sF0))),
    inference(forward_demodulation,[],[f119991,f23626]) ).

fof(f120039,plain,
    sF5 = double_divide(double_divide(identity,c3),double_divide(identity,double_divide(sF0,double_divide(b3,double_divide(b3,a3))))),
    inference(forward_demodulation,[],[f120020,f23629]) ).

fof(f120056,plain,
    sF5 = double_divide(identity,double_divide(c3,double_divide(sF0,double_divide(b3,double_divide(b3,a3))))),
    inference(forward_demodulation,[],[f120039,f63774]) ).

fof(f120068,plain,
    sF5 = double_divide(identity,double_divide(c3,double_divide(sF0,a3))),
    inference(forward_demodulation,[],[f120056,f7659]) ).

fof(f120077,plain,
    sF5 = double_divide(identity,double_divide(c3,double_divide(a3,sF0))),
    inference(forward_demodulation,[],[f120068,f23626]) ).

fof(f120085,plain,
    sF5 = double_divide(a3,sF2),
    inference(forward_demodulation,[],[f120077,f56905]) ).

fof(f120884,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(sF2,identity))) = double_divide(double_divide(X0,sF5),double_divide(double_divide(identity,double_divide(identity,a3)),double_divide(identity,double_divide(identity,double_divide(X0,identity))))),
    inference(superposition,[],[f714,f120085]) ).

fof(f120907,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(sF2,identity))) = double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(X0,identity))),double_divide(double_divide(identity,a3),double_divide(X0,sF5)))),
    inference(forward_demodulation,[],[f120884,f23629]) ).

fof(f120940,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(sF2,identity))) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(double_divide(double_divide(identity,a3),double_divide(X0,sF5)),identity)),
    inference(forward_demodulation,[],[f120907,f23749]) ).

fof(f120973,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(sF2,identity))) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(identity,double_divide(double_divide(identity,a3),double_divide(X0,sF5)))),
    inference(forward_demodulation,[],[f120940,f11149]) ).

fof(f121006,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(sF2,identity))) = double_divide(identity,double_divide(double_divide(X0,identity),double_divide(double_divide(identity,a3),double_divide(X0,sF5)))),
    inference(forward_demodulation,[],[f120973,f63774]) ).

fof(f121037,plain,
    ! [X0] : double_divide(identity,double_divide(identity,double_divide(sF2,identity))) = double_divide(X0,double_divide(identity,double_divide(double_divide(identity,a3),double_divide(X0,sF5)))),
    inference(forward_demodulation,[],[f121006,f56701]) ).

fof(f121065,plain,
    double_divide(identity,double_divide(identity,double_divide(sF2,identity))) = double_divide(double_divide(identity,a3),double_divide(identity,sF5)),
    inference(forward_demodulation,[],[f121037,f83818]) ).

fof(f121092,plain,
    double_divide(identity,double_divide(identity,double_divide(sF2,identity))) = double_divide(identity,double_divide(a3,sF5)),
    inference(forward_demodulation,[],[f121065,f63774]) ).

fof(f121110,plain,
    sF7 = double_divide(identity,double_divide(identity,double_divide(sF2,identity))),
    inference(forward_demodulation,[],[f121092,f6097]) ).

fof(f121121,plain,
    double_divide(sF2,identity) = sF7,
    inference(forward_demodulation,[],[f121110,f7659]) ).

fof(f121127,plain,
    sF7 = double_divide(identity,sF2),
    inference(forward_demodulation,[],[f121121,f2759]) ).

fof(f121130,plain,
    sF3 = sF7,
    inference(forward_demodulation,[],[f121127,f2763]) ).

fof(f121131,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f121130,f24]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP583-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39  % Computer : n009.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:45 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.42  Running first-order model finding
% 0.12/0.42  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
% 15.29/2.70  % (1795659)Will run a generic schedule for satisfiability detection.
% 15.29/2.70  % (1795677)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2800207453:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.29/2.70  % (1795674)% WARNING: option uhcvi not known.
% 15.29/2.70  % (1795673)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1946816283_2999 on theBenchmark for (2999ds/0Mi)
% 15.29/2.70  % (1795676)dis+10_1_sil=32000:sp=arity:random_seed=1799432068:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.29/2.70  % (1795674)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=30173907:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.29/2.70  % (1795675)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3673257318:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.29/2.70  % (1795680)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=949789991:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.29/2.70  % (1795679)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2025738285:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.29/2.70  % TRYING [1]
% 15.29/2.70  % TRYING [2]
% 15.29/2.70  % TRYING [3]
% 15.29/2.70  % TRYING [4]
% 15.29/2.70  % TRYING [5]
% 15.29/2.70  % (1795677)Instruction limit reached! 
% 15.29/2.70  % (1795677)------------------------------
% 15.29/2.70  % (1795677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.29/2.70  % (1795677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/2.70  % (1795677)CaDiCaL version: 2.1.3
% 15.29/2.70  % (1795677)Termination reason: Instruction limit
% 15.29/2.70  % (1795677)Termination phase: Saturation
% 15.29/2.70  % (1795677)Time elapsed: 0.037 s
% 15.29/2.70  % (1795677)Peak memory usage: 12 MB
% 15.29/2.70  % (1795677)Instructions burned: 119 (million)
% 15.29/2.70  % (1795708)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1950461042:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.29/2.70  % TRYING [1]
% 15.29/2.70  % TRYING [2]
% 15.29/2.70  % TRYING [3]
% 15.29/2.70  % TRYING [4]
% 15.29/2.70  % TRYING [6]
% 15.29/2.70  % TRYING [5]
% 15.29/2.70  % (1795676)Instruction limit reached! 
% 15.29/2.70  % (1795676)------------------------------
% 15.29/2.70  % (1795676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.29/2.70  % (1795676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/2.70  % (1795676)CaDiCaL version: 2.1.3
% 15.29/2.70  % (1795676)Termination reason: Instruction limit
% 15.29/2.70  % (1795676)Termination phase: Saturation
% 15.29/2.70  % (1795676)Time elapsed: 0.059 s
% 15.29/2.70  % (1795676)Peak memory usage: 12 MB
% 15.29/2.70  % (1795676)Instructions burned: 109 (million)
% 15.29/2.70  % (1795679)Instruction limit reached! 
% 15.29/2.70  % (1795679)------------------------------
% 15.29/2.70  % (1795679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.29/2.70  % (1795679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/2.70  % (1795679)CaDiCaL version: 2.1.3
% 15.29/2.70  % (1795679)Termination reason: Instruction limit
% 15.29/2.70  % (1795679)Termination phase: Saturation
% 15.29/2.70  % (1795679)Time elapsed: 0.073 s
% 15.29/2.70  % (1795679)Peak memory usage: 13 MB
% 15.29/2.70  % (1795679)Instructions burned: 131 (million)
% 15.29/2.70  % (1795718)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=846929561:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.29/2.70  % TRYING [6]
% 15.29/2.70  % (1795680)Instruction limit reached! 
% 15.29/2.70  % (1795680)------------------------------
% 15.29/2.70  % (1795680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.29/2.70  % (1795680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/2.70  % (1795680)CaDiCaL version: 2.1.3
% 15.29/2.70  % (1795680)Termination reason: Instruction limit
% 15.29/2.70  % (1795680)Termination phase: Saturation
% 15.29/2.70  % (1795680)Time elapsed: 0.094 s
% 15.29/2.70  % (1795680)Peak memory usage: 12 MB
% 15.29/2.70  % (1795680)Instructions burned: 159 (million)
% 15.29/2.70  % (1795725)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=3793112535:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.29/2.70  % (1795732)ott-21_1_sil=16000:fs=off:random_seed=4150737527:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.29/2.70  % (1795718)Instruction limit reached! 
% 15.29/2.70  % (1795718)------------------------------
% 15.29/2.70  % (1795718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795718)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795718)Termination reason: Instruction limit
% 45.82/7.22  % (1795718)Termination phase: Saturation
% 45.82/7.22  % (1795718)Time elapsed: 0.082 s
% 45.82/7.22  % (1795718)Peak memory usage: 12 MB
% 45.82/7.22  % (1795718)Instructions burned: 133 (million)
% 45.82/7.22  % (1795758)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2796224116:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 45.82/7.22  % (1795732)Instruction limit reached! 
% 45.82/7.22  % (1795732)------------------------------
% 45.82/7.22  % (1795732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795732)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795732)Termination reason: Instruction limit
% 45.82/7.22  % (1795732)Termination phase: Saturation
% 45.82/7.22  % (1795732)Time elapsed: 0.076 s
% 45.82/7.22  % (1795732)Peak memory usage: 12 MB
% 45.82/7.22  % (1795732)Instructions burned: 180 (million)
% 45.82/7.22  % TRYING [7]
% 45.82/7.22  % (1795763)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4023121820:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 45.82/7.22  % TRYING [1]
% 45.82/7.22  % TRYING [2]
% 45.82/7.22  % TRYING [3]
% 45.82/7.22  % TRYING [4]
% 45.82/7.22  % TRYING [5]
% 45.82/7.22  % TRYING [7]
% 45.82/7.22  % (1795708)Instruction limit reached! 
% 45.82/7.22  % (1795708)------------------------------
% 45.82/7.22  % (1795708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795708)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795708)Termination reason: Instruction limit
% 45.82/7.22  % (1795708)Termination phase: Finite model building constraint generation
% 45.82/7.22  % (1795708)Time elapsed: 0.219 s
% 45.82/7.22  % (1795708)Peak memory usage: 18 MB
% 45.82/7.22  % (1795708)Instructions burned: 720 (million)
% 45.82/7.22  % TRYING [6]
% 45.82/7.22  % (1795783)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=213741397:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 45.82/7.22  % TRYING [7]
% 45.82/7.22  % (1795758)Instruction limit reached! 
% 45.82/7.22  % (1795758)------------------------------
% 45.82/7.22  % (1795758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795758)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795758)Termination reason: Instruction limit
% 45.82/7.22  % (1795758)Termination phase: Saturation
% 45.82/7.22  % (1795758)Time elapsed: 0.259 s
% 45.82/7.22  % (1795758)Peak memory usage: 14 MB
% 45.82/7.22  % (1795758)Instructions burned: 477 (million)
% 45.82/7.22  % (1795725)Instruction limit reached! 
% 45.82/7.22  % (1795725)------------------------------
% 45.82/7.22  % (1795725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795725)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795725)Termination reason: Instruction limit
% 45.82/7.22  % (1795725)Termination phase: Saturation
% 45.82/7.22  % (1795725)Time elapsed: 0.352 s
% 45.82/7.22  % (1795725)Peak memory usage: 15 MB
% 45.82/7.22  % (1795725)Instructions burned: 684 (million)
% 45.82/7.22  % (1795843)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1272544252:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 45.82/7.22  % (1795844)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=137999686:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 45.82/7.22  % TRYING [14]
% 45.82/7.22  % (1795763)Instruction limit reached! 
% 45.82/7.22  % (1795763)------------------------------
% 45.82/7.22  % (1795763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795763)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795763)Termination reason: Instruction limit
% 45.82/7.22  % (1795763)Termination phase: Finite model building SAT solving
% 45.82/7.22  % (1795763)Time elapsed: 0.368 s
% 45.82/7.22  % (1795763)Peak memory usage: 17 MB
% 45.82/7.22  % (1795763)Instructions burned: 865 (million)
% 45.82/7.22  % (1795847)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4262831177:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 45.82/7.22  % (1795783)Instruction limit reached! 
% 45.82/7.22  % (1795783)------------------------------
% 45.82/7.22  % (1795783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795783)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795783)Termination reason: Instruction limit
% 45.82/7.22  % (1795783)Termination phase: Saturation
% 45.82/7.22  % (1795783)Time elapsed: 0.358 s
% 45.82/7.22  % (1795783)Peak memory usage: 20 MB
% 45.82/7.22  % (1795783)Instructions burned: 1181 (million)
% 45.82/7.22  % (1795849)fmb+10_1_sil=64000:random_seed=3439595744:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 45.82/7.22  % TRYING [1]
% 45.82/7.22  % TRYING [2]
% 45.82/7.22  % TRYING [3]
% 45.82/7.22  % TRYING [4]
% 45.82/7.22  % TRYING [5]
% 45.82/7.22  % TRYING [6]
% 45.82/7.22  % TRYING [7]
% 45.82/7.22  % (1795843)Instruction limit reached! 
% 45.82/7.22  % (1795843)------------------------------
% 45.82/7.22  % (1795843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795843)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795843)Termination reason: Instruction limit
% 45.82/7.22  % (1795843)Termination phase: Finite model building constraint generation
% 45.82/7.22  % (1795843)Time elapsed: 0.320 s
% 45.82/7.22  % (1795843)Peak memory usage: 80 MB
% 45.82/7.22  % (1795843)Instructions burned: 890 (million)
% 45.82/7.22  % (1795851)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2175027439:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 45.82/7.22  % TRYING [20]
% 45.82/7.22  % (1795844)Instruction limit reached! 
% 45.82/7.22  % (1795844)------------------------------
% 45.82/7.22  % (1795844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795844)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795844)Termination reason: Instruction limit
% 45.82/7.22  % (1795844)Termination phase: Saturation
% 45.82/7.22  % (1795844)Time elapsed: 0.401 s
% 45.82/7.22  % (1795844)Peak memory usage: 15 MB
% 45.82/7.22  % (1795844)Instructions burned: 692 (million)
% 45.82/7.22  % TRYING [8]
% 45.82/7.22  % (1795853)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1665811190:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 45.82/7.22  % TRYING [8]
% 45.82/7.22  % (1795847)Instruction limit reached! 
% 45.82/7.22  % (1795847)------------------------------
% 45.82/7.22  % (1795847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % TRYING [8]
% 45.82/7.22  % (1795847)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795847)Termination reason: Instruction limit
% 45.82/7.22  % (1795847)Termination phase: Saturation
% 45.82/7.22  % (1795847)Time elapsed: 0.465 s
% 45.82/7.22  % (1795847)Peak memory usage: 16 MB
% 45.82/7.22  % (1795847)Instructions burned: 881 (million)
% 45.82/7.22  % (1795855)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1128165087:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 45.82/7.22  % (1795853)Instruction limit reached! 
% 45.82/7.22  % (1795853)------------------------------
% 45.82/7.22  % (1795853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795853)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795853)Termination reason: Instruction limit
% 45.82/7.22  % (1795853)Termination phase: Finite model building SAT solving
% 45.82/7.22  % (1795853)Time elapsed: 0.529 s
% 45.82/7.22  % (1795853)Peak memory usage: 36 MB
% 45.82/7.22  % (1795853)Instructions burned: 920 (million)
% 45.82/7.22  % (1795857)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3883413884:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 45.82/7.22  % (1795857)Instruction limit reached! 
% 45.82/7.22  % (1795857)------------------------------
% 45.82/7.22  % (1795857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795857)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795857)Termination reason: Instruction limit
% 45.82/7.22  % (1795857)Termination phase: Saturation
% 45.82/7.22  % (1795857)Time elapsed: 0.755 s
% 45.82/7.22  % (1795857)Peak memory usage: 28 MB
% 45.82/7.22  % (1795857)Instructions burned: 1473 (million)
% 45.82/7.22  % (1795859)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=431313762:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 45.82/7.22  % TRYING [77]
% 45.82/7.22  % TRYING [9]
% 45.82/7.22  % (1795855)Instruction limit reached! 
% 45.82/7.22  % (1795855)------------------------------
% 45.82/7.22  % (1795855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795855)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795855)Termination reason: Instruction limit
% 45.82/7.22  % (1795855)Termination phase: Saturation
% 45.82/7.22  % (1795855)Time elapsed: 2.837 s
% 45.82/7.22  % (1795855)Peak memory usage: 44 MB
% 45.82/7.22  % (1795855)Instructions burned: 5134 (million)
% 45.82/7.22  % (1795861)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1214941534:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 45.82/7.22  % TRYING [16]
% 45.82/7.22  % (1795851)Instruction limit reached! 
% 45.82/7.22  % (1795851)------------------------------
% 45.82/7.22  % (1795851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795851)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795851)Termination reason: Instruction limit
% 45.82/7.22  % (1795851)Termination phase: Finite model building constraint generation
% 45.82/7.22  % (1795851)Time elapsed: 3.636 s
% 45.82/7.22  % (1795851)Peak memory usage: 631 MB
% 45.82/7.22  % (1795851)Instructions burned: 9517 (million)
% 45.82/7.22  % (1795863)ott-2_1_sil=16000:newcnf=on:random_seed=2577374057:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2954 on theBenchmark for (2954ds/869Mi)
% 45.82/7.22  % (1795859)Instruction limit reached! 
% 45.82/7.22  % (1795859)------------------------------
% 45.82/7.22  % (1795859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795859)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795859)Termination reason: Instruction limit
% 45.82/7.22  % (1795859)Termination phase: Finite model building constraint generation
% 45.82/7.22  % (1795859)Time elapsed: 2.371 s
% 45.82/7.22  % (1795859)Peak memory usage: 522 MB
% 45.82/7.22  % (1795859)Instructions burned: 6325 (million)
% 45.82/7.22  % (1795865)ott+10_1_sil=32000:tgt=ground:random_seed=1381041141:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 45.82/7.22  % TRYING [9]
% 45.82/7.22  % (1795861)Instruction limit reached! 
% 45.82/7.22  % (1795861)------------------------------
% 45.82/7.22  % (1795861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795861)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795861)Termination reason: Instruction limit
% 45.82/7.22  % (1795861)Termination phase: Finite model building constraint generation
% 45.82/7.22  % (1795861)Time elapsed: 0.789 s
% 45.82/7.22  % (1795861)Peak memory usage: 155 MB
% 45.82/7.22  % (1795861)Instructions burned: 2176 (million)
% 45.82/7.22  % (1795867)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=106690951:i=54282_2952 on theBenchmark for (2952ds/54282Mi)
% 45.82/7.22  % TRYING [1]
% 45.82/7.22  % TRYING [2]
% 45.82/7.22  % TRYING [3]
% 45.82/7.22  % TRYING [4]
% 45.82/7.22  % TRYING [5]
% 45.82/7.22  % TRYING [6]
% 45.82/7.22  % TRYING [7]
% 45.82/7.22  % (1795863)Instruction limit reached! 
% 45.82/7.22  % (1795863)------------------------------
% 45.82/7.22  % (1795863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795863)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795863)Termination reason: Instruction limit
% 45.82/7.22  % (1795863)Termination phase: Saturation
% 45.82/7.22  % (1795863)Time elapsed: 0.501 s
% 45.82/7.22  % (1795863)Peak memory usage: 18 MB
% 45.82/7.22  % (1795863)Instructions burned: 871 (million)
% 45.82/7.22  % (1795869)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2019609193:i=3512:aac=none_2949 on theBenchmark for (2949ds/3512Mi)
% 45.82/7.22  % TRYING [8]
% 45.82/7.22  % (1795865) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1795659-1795865"...
% 45.82/7.22  % (1795865)...printing done.
% 45.82/7.22  % (1795865)Refutation found. Thanks to Tanya!
% 45.82/7.22  % SZS status Unsatisfiable for theBenchmark
% 45.82/7.22  % SZS output start Proof for theBenchmark
% See solution above
% 45.82/7.22  % (1795865)------------------------------
% 45.82/7.22  % (1795865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.82/7.22  % (1795865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.82/7.22  % (1795865)CaDiCaL version: 2.1.3
% 45.82/7.22  % (1795865)Termination reason: Refutation
% 45.82/7.22  % (1795865)Time elapsed: 2.051 s
% 45.82/7.22  % (1795865)Peak memory usage: 42 MB
% 45.82/7.22  % (1795865)Instructions burned: 3691 (million)
% 45.82/7.22  % (1795659)Success in time 6.785 s
% 45.82/7.22  % Vampire exiting
%------------------------------------------------------------------------------