%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP100-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:12:35 AM UTC 2026
% Result : Unsatisfiable 6.89s 2.01s
% Output : Refutation 8.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 5
% Syntax : Number of formulae : 230 ( 209 unt; 0 def)
% Number of atoms : 272 ( 271 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 107 ( 65 ~; 42 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 606 ( 606 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(X2,identity))),double_divide(identity,identity)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,axiom,
! [X0,X1] : multiply(X0,X1) = double_divide(double_divide(X1,X0),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
fof(f3,axiom,
! [X0] : inverse(X0) = double_divide(X0,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse) ).
fof(f4,axiom,
! [X0] : identity = double_divide(X0,inverse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity) ).
fof(f5,negated_conjecture,
( multiply(inverse(a1),a1) != identity
| multiply(identity,a2) != a2
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(a4,b4) != multiply(b4,a4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f6,plain,
( identity != multiply(inverse(a1),a1)
| a2 != multiply(identity,a2)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(a4,b4) != multiply(b4,a4) ),
inference(reorient_equations,[],[f5]) ).
fof(f7,plain,
! [X0] : identity = double_divide(X0,double_divide(X0,identity)),
inference(definition_unfolding,[],[f4,f3]) ).
fof(f8,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)
| a2 != double_divide(double_divide(a2,identity),identity)
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(definition_unfolding,[],[f6,f2,f3,f2,f2,f2,f2,f2,f2,f2]) ).
fof(f10,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X2,identity))) = double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f1,f1]) ).
fof(f11,plain,
! [X0] : double_divide(double_divide(X0,double_divide(identity,double_divide(identity,identity))),double_divide(identity,identity)) = X0,
inference(superposition,[],[f1,f7]) ).
fof(f13,plain,
! [X0] : double_divide(double_divide(X0,identity),double_divide(identity,identity)) = X0,
inference(forward_demodulation,[],[f11,f7]) ).
fof(f14,plain,
! [X0] : double_divide(X0,identity) = double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f1,f13]) ).
fof(f31,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X1,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),double_divide(double_divide(X2,identity),identity))),
inference(superposition,[],[f10,f10]) ).
fof(f51,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X1,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(X0,identity),double_divide(double_divide(X2,identity),identity))),
inference(forward_demodulation,[],[f31,f14]) ).
fof(f60,plain,
! [X2,X0,X1] : double_divide(X1,identity) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(X0,identity),double_divide(double_divide(X2,identity),identity))),
inference(forward_demodulation,[],[f51,f14]) ).
fof(f78,plain,
! [X0,X1] : double_divide(X0,identity) = double_divide(double_divide(X1,double_divide(X0,X1)),identity),
inference(superposition,[],[f60,f7]) ).
fof(f103,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(identity,double_divide(X2,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(X1,double_divide(double_divide(X2,double_divide(X1,double_divide(X3,double_divide(X0,X3)))),double_divide(X0,identity))),
inference(superposition,[],[f10,f78]) ).
fof(f106,plain,
! [X0,X1] : double_divide(double_divide(X0,identity),double_divide(identity,identity)) = double_divide(X1,double_divide(X0,X1)),
inference(superposition,[],[f13,f78]) ).
fof(f113,plain,
! [X0,X1] : double_divide(X1,double_divide(X0,X1)) = X0,
inference(forward_demodulation,[],[f106,f13]) ).
fof(f115,plain,
! [X2,X3,X0,X1] : double_divide(X2,identity) = double_divide(X1,double_divide(double_divide(X2,double_divide(X1,double_divide(X3,double_divide(X0,X3)))),double_divide(X0,identity))),
inference(forward_demodulation,[],[f103,f14]) ).
fof(f120,plain,
! [X2,X0,X1] : double_divide(X2,identity) = double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X0)),double_divide(X0,identity))),
inference(forward_demodulation,[],[f115,f113]) ).
fof(f123,plain,
! [X0] : double_divide(X0,identity) = double_divide(double_divide(identity,identity),X0),
inference(superposition,[],[f113,f13]) ).
fof(f124,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(double_divide(identity,identity),double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(X2,identity)))),
inference(superposition,[],[f113,f10]) ).
fof(f125,plain,
! [X0] : double_divide(double_divide(X0,identity),identity) = X0,
inference(superposition,[],[f113,f7]) ).
fof(f128,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),X0) = X1,
inference(superposition,[],[f113,f113]) ).
fof(f148,plain,
! [X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(double_divide(identity,identity),double_divide(X1,identity)),
inference(forward_demodulation,[],[f124,f120]) ).
fof(f151,plain,
! [X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(double_divide(X1,identity),identity),
inference(forward_demodulation,[],[f148,f123]) ).
fof(f152,plain,
! [X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = X1,
inference(forward_demodulation,[],[f151,f125]) ).
fof(f157,plain,
! [X0] : double_divide(X0,identity) = double_divide(identity,X0),
inference(superposition,[],[f128,f7]) ).
fof(f158,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X2,identity)) = double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),X1),
inference(superposition,[],[f128,f10]) ).
fof(f159,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),double_divide(double_divide(X2,identity),identity)) = double_divide(double_divide(X0,identity),double_divide(X1,double_divide(X0,X2))),
inference(superposition,[],[f128,f60]) ).
fof(f165,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(X1,identity),double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(X0,double_divide(X0,X1)),
inference(superposition,[],[f10,f128]) ).
fof(f166,plain,
! [X0,X1] : double_divide(X1,identity) = double_divide(double_divide(X0,double_divide(X0,X1)),double_divide(identity,identity)),
inference(superposition,[],[f1,f128]) ).
fof(f167,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(double_divide(identity,identity),X1)),double_divide(X1,identity)) = X0,
inference(superposition,[],[f1,f128]) ).
fof(f178,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(double_divide(X1,X2),X0),double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(X1,double_divide(X0,double_divide(X2,identity))),
inference(superposition,[],[f10,f128]) ).
fof(f179,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,X2),X0) = double_divide(double_divide(X1,double_divide(X0,double_divide(X2,identity))),double_divide(identity,identity)),
inference(superposition,[],[f1,f128]) ).
fof(f186,plain,
! [X0] : double_divide(X0,double_divide(identity,identity)) = double_divide(identity,X0),
inference(superposition,[],[f13,f128]) ).
fof(f195,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,X2),X0) = double_divide(identity,double_divide(X1,double_divide(X0,double_divide(X2,identity)))),
inference(forward_demodulation,[],[f179,f186]) ).
fof(f196,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,double_divide(X2,identity))) = double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(X1,X2),X0),double_divide(identity,identity)))),
inference(forward_demodulation,[],[f178,f186]) ).
fof(f206,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(X1,identity)),double_divide(X1,identity)) = X0,
inference(forward_demodulation,[],[f167,f123]) ).
fof(f207,plain,
! [X0,X1] : double_divide(X1,identity) = double_divide(identity,double_divide(X0,double_divide(X0,X1))),
inference(forward_demodulation,[],[f166,f186]) ).
fof(f208,plain,
! [X0,X1] : double_divide(X0,double_divide(X0,X1)) = double_divide(identity,double_divide(identity,double_divide(double_divide(X1,identity),double_divide(identity,identity)))),
inference(forward_demodulation,[],[f165,f186]) ).
fof(f212,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(X1,double_divide(X0,X2))) = double_divide(double_divide(X1,identity),X2),
inference(forward_demodulation,[],[f159,f125]) ).
fof(f213,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X2,identity)) = double_divide(double_divide(identity,double_divide(identity,double_divide(X0,double_divide(identity,identity)))),X1),
inference(forward_demodulation,[],[f158,f186]) ).
fof(f221,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,double_divide(X2,identity))) = double_divide(double_divide(identity,identity),double_divide(double_divide(X1,X2),X0)),
inference(forward_demodulation,[],[f196,f195]) ).
fof(f227,plain,
! [X0,X1] : double_divide(double_divide(identity,identity),double_divide(X1,identity)) = double_divide(X0,double_divide(X0,X1)),
inference(forward_demodulation,[],[f208,f195]) ).
fof(f228,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X2,identity)) = double_divide(double_divide(double_divide(identity,identity),X0),X1),
inference(forward_demodulation,[],[f213,f195]) ).
fof(f234,plain,
! [X2,X0,X1] : double_divide(double_divide(double_divide(X1,X2),X0),identity) = double_divide(X1,double_divide(X0,double_divide(X2,identity))),
inference(forward_demodulation,[],[f221,f123]) ).
fof(f237,plain,
! [X0,X1] : double_divide(double_divide(X1,identity),identity) = double_divide(X0,double_divide(X0,X1)),
inference(forward_demodulation,[],[f227,f123]) ).
fof(f238,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X2,identity)) = double_divide(double_divide(X0,identity),X1),
inference(forward_demodulation,[],[f228,f123]) ).
fof(f241,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,double_divide(X2,identity))) = double_divide(identity,double_divide(double_divide(X1,X2),X0)),
inference(forward_demodulation,[],[f234,f157]) ).
fof(f242,plain,
! [X0,X1] : double_divide(X0,double_divide(X0,X1)) = double_divide(identity,double_divide(X1,identity)),
inference(forward_demodulation,[],[f237,f157]) ).
fof(f244,plain,
! [X0,X1] : double_divide(X0,double_divide(X0,X1)) = X1,
inference(forward_demodulation,[],[f242,f113]) ).
fof(f246,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X2,identity)) = double_divide(X1,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity))),
inference(superposition,[],[f244,f10]) ).
fof(f264,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(X0,X1),
inference(superposition,[],[f128,f244]) ).
fof(f284,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X2,identity)) = double_divide(X1,double_divide(identity,double_divide(identity,double_divide(X0,double_divide(identity,identity))))),
inference(forward_demodulation,[],[f246,f186]) ).
fof(f298,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X2,identity)) = double_divide(X1,double_divide(X0,double_divide(identity,identity))),
inference(forward_demodulation,[],[f284,f244]) ).
fof(f308,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X2,identity)) = double_divide(X1,double_divide(identity,X0)),
inference(forward_demodulation,[],[f298,f186]) ).
fof(f312,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(identity,X0)) = double_divide(double_divide(X2,identity),double_divide(X0,double_divide(X1,X2))),
inference(forward_demodulation,[],[f308,f264]) ).
fof(f1017,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),double_divide(X2,X0)) = double_divide(double_divide(X1,X0),double_divide(X2,identity)),
inference(superposition,[],[f238,f128]) ).
fof(f1022,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(X1,X0),double_divide(double_divide(X0,X2),identity)),
inference(superposition,[],[f238,f113]) ).
fof(f1025,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(X1,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity))),double_divide(double_divide(double_divide(X0,double_divide(X2,X3)),double_divide(X3,identity)),identity)),
inference(superposition,[],[f238,f10]) ).
fof(f1030,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(X2,identity)))),double_divide(double_divide(identity,identity),identity)) = double_divide(double_divide(X3,identity),double_divide(identity,double_divide(X1,double_divide(identity,identity)))),
inference(superposition,[],[f238,f10]) ).
fof(f1031,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(X0,double_divide(X1,X3))) = double_divide(double_divide(X2,double_divide(double_divide(X0,identity),X1)),double_divide(double_divide(X3,identity),identity)),
inference(superposition,[],[f238,f238]) ).
fof(f1032,plain,
! [X0,X1] : double_divide(double_divide(X0,identity),double_divide(double_divide(X1,identity),identity)) = double_divide(double_divide(X0,identity),X1),
inference(superposition,[],[f238,f7]) ).
fof(f1034,plain,
! [X0,X1] : double_divide(double_divide(X1,identity),double_divide(X0,identity)) = double_divide(double_divide(X1,X0),double_divide(identity,identity)),
inference(superposition,[],[f238,f125]) ).
fof(f1035,plain,
! [X0,X1] : double_divide(double_divide(X1,double_divide(identity,X0)),double_divide(identity,identity)) = double_divide(double_divide(X1,identity),X0),
inference(superposition,[],[f238,f157]) ).
fof(f1039,plain,
! [X2,X0,X1] : double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),double_divide(double_divide(X2,identity),identity)) = double_divide(double_divide(X1,identity),double_divide(X0,double_divide(X1,X2))),
inference(superposition,[],[f238,f10]) ).
fof(f1040,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(double_divide(double_divide(X2,identity),identity),identity)) = double_divide(double_divide(double_divide(X1,double_divide(X0,X2)),identity),double_divide(X1,identity)),
inference(superposition,[],[f238,f60]) ).
fof(f1047,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X2,identity)) = double_divide(double_divide(double_divide(double_divide(X1,X2),X0),identity),X1),
inference(superposition,[],[f238,f128]) ).
fof(f1054,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(X1,double_divide(X2,double_divide(identity,X0))),X0),
inference(superposition,[],[f238,f128]) ).
fof(f1057,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(X1,double_divide(X2,X0)),double_divide(identity,X0)),
inference(superposition,[],[f238,f264]) ).
fof(f1065,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(X2,double_divide(double_divide(double_divide(X0,identity),X1),double_divide(identity,identity))),
inference(superposition,[],[f10,f238]) ).
fof(f1067,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(double_divide(double_divide(X0,double_divide(X1,identity)),double_divide(X2,X3)),double_divide(X3,identity))) = double_divide(double_divide(identity,double_divide(double_divide(X0,identity),X1)),double_divide(identity,identity)),
inference(superposition,[],[f10,f238]) ).
fof(f1072,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X1,X2)) = double_divide(double_divide(X2,identity),double_divide(double_divide(X0,identity),X1)),
inference(superposition,[],[f113,f238]) ).
fof(f1082,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(double_divide(double_divide(X0,double_divide(X1,identity)),double_divide(X2,X3)),double_divide(X3,identity))) = double_divide(identity,double_divide(identity,double_divide(double_divide(X0,identity),X1))),
inference(forward_demodulation,[],[f1067,f186]) ).
fof(f1084,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(X2,double_divide(identity,double_divide(double_divide(X0,identity),X1))),
inference(forward_demodulation,[],[f1065,f186]) ).
fof(f1090,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(identity,X0),double_divide(X1,double_divide(X2,X0))),
inference(forward_demodulation,[],[f1057,f264]) ).
fof(f1093,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(X0,double_divide(X1,double_divide(X2,double_divide(identity,X0)))),
inference(forward_demodulation,[],[f1054,f264]) ).
fof(f1100,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X2,identity)) = double_divide(X1,double_divide(double_divide(double_divide(X1,X2),X0),identity)),
inference(forward_demodulation,[],[f1047,f264]) ).
fof(f1107,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(double_divide(double_divide(X2,identity),identity),identity)) = double_divide(double_divide(X1,identity),double_divide(double_divide(X1,double_divide(X0,X2)),identity)),
inference(forward_demodulation,[],[f1040,f264]) ).
fof(f1108,plain,
! [X2,X0] : double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),double_divide(double_divide(X2,identity),identity)) = double_divide(double_divide(X0,identity),X2),
inference(forward_demodulation,[],[f1039,f212]) ).
fof(f1111,plain,
! [X0,X1] : double_divide(identity,double_divide(X1,double_divide(identity,X0))) = double_divide(double_divide(X1,identity),X0),
inference(forward_demodulation,[],[f1035,f186]) ).
fof(f1112,plain,
! [X0,X1] : double_divide(double_divide(X1,identity),double_divide(X0,identity)) = double_divide(identity,double_divide(X1,X0)),
inference(forward_demodulation,[],[f1034,f186]) ).
fof(f1114,plain,
! [X0,X1] : double_divide(X1,double_divide(identity,X0)) = double_divide(double_divide(X0,identity),X1),
inference(forward_demodulation,[],[f1032,f1072]) ).
fof(f1115,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(X0,double_divide(X1,X3))) = double_divide(double_divide(X2,double_divide(double_divide(X0,identity),X1)),double_divide(identity,double_divide(X3,identity))),
inference(forward_demodulation,[],[f1031,f157]) ).
fof(f1116,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(X2,identity)))),double_divide(double_divide(identity,identity),identity)) = double_divide(double_divide(X3,identity),X1),
inference(forward_demodulation,[],[f1030,f152]) ).
fof(f1121,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(X1,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity))),double_divide(identity,double_divide(double_divide(X0,double_divide(X2,X3)),double_divide(X3,identity)))),
inference(forward_demodulation,[],[f1025,f157]) ).
fof(f1124,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(X1,X0),double_divide(identity,double_divide(X0,X2))),
inference(forward_demodulation,[],[f1022,f157]) ).
fof(f1133,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X0,identity),X1) = double_divide(X2,double_divide(double_divide(double_divide(X0,double_divide(X1,identity)),double_divide(X2,X3)),double_divide(X3,identity))),
inference(forward_demodulation,[],[f1082,f244]) ).
fof(f1135,plain,
! [X2,X0,X1] : double_divide(X2,double_divide(identity,double_divide(double_divide(X0,identity),X1))) = double_divide(identity,double_divide(identity,double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(identity,identity)))),
inference(forward_demodulation,[],[f1084,f186]) ).
fof(f1142,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X2,identity)) = double_divide(X1,double_divide(identity,double_divide(double_divide(X1,X2),X0))),
inference(forward_demodulation,[],[f1100,f157]) ).
fof(f1149,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(double_divide(double_divide(X2,identity),identity),identity)) = double_divide(double_divide(X1,identity),double_divide(identity,double_divide(X1,double_divide(X0,X2)))),
inference(forward_demodulation,[],[f1107,f157]) ).
fof(f1150,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),X2) = double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),identity),double_divide(double_divide(X2,identity),double_divide(identity,identity))),
inference(forward_demodulation,[],[f1108,f1017]) ).
fof(f1153,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(X0,double_divide(X1,X3))) = double_divide(identity,double_divide(double_divide(double_divide(X2,double_divide(double_divide(X0,identity),X1)),X3),identity)),
inference(forward_demodulation,[],[f1115,f241]) ).
fof(f1154,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),X1) = double_divide(double_divide(double_divide(identity,identity),identity),double_divide(X3,double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(X2,identity))))),
inference(forward_demodulation,[],[f1116,f264]) ).
fof(f1159,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(X1,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity))),double_divide(identity,double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X2,X3))))),
inference(forward_demodulation,[],[f1121,f241]) ).
fof(f1164,plain,
! [X0,X1] : double_divide(double_divide(X0,identity),X1) = double_divide(double_divide(X0,double_divide(X1,identity)),identity),
inference(forward_demodulation,[],[f1133,f120]) ).
fof(f1165,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(identity,identity)) = double_divide(X2,double_divide(identity,double_divide(double_divide(X0,identity),X1))),
inference(forward_demodulation,[],[f1135,f244]) ).
fof(f1172,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),double_divide(double_divide(double_divide(X2,identity),identity),identity)) = double_divide(double_divide(identity,identity),double_divide(X0,X2)),
inference(forward_demodulation,[],[f1149,f212]) ).
fof(f1173,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),X2) = double_divide(identity,double_divide(double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),identity),identity),double_divide(X2,identity))),
inference(forward_demodulation,[],[f1150,f241]) ).
fof(f1174,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(X0,double_divide(X1,X3))) = double_divide(double_divide(X2,double_divide(double_divide(X0,identity),X1)),X3),
inference(forward_demodulation,[],[f1153,f113]) ).
fof(f1175,plain,
! [X3,X1] : double_divide(double_divide(X3,identity),X1) = double_divide(double_divide(double_divide(identity,identity),identity),double_divide(X3,double_divide(X1,identity))),
inference(forward_demodulation,[],[f1154,f120]) ).
fof(f1180,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(X1,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity))),double_divide(identity,double_divide(double_divide(X0,identity),X2))),
inference(forward_demodulation,[],[f1159,f1090]) ).
fof(f1184,plain,
! [X0,X1] : double_divide(double_divide(X0,identity),X1) = double_divide(identity,double_divide(X0,double_divide(X1,identity))),
inference(forward_demodulation,[],[f1164,f157]) ).
fof(f1185,plain,
! [X2,X0,X1] : double_divide(X2,double_divide(identity,double_divide(double_divide(X0,identity),X1))) = double_divide(identity,double_divide(X0,double_divide(X1,X2))),
inference(forward_demodulation,[],[f1165,f186]) ).
fof(f1189,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),double_divide(double_divide(double_divide(X2,identity),identity),identity)) = double_divide(double_divide(X0,X2),identity),
inference(forward_demodulation,[],[f1172,f123]) ).
fof(f1190,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),X2) = double_divide(identity,double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),identity),X2))),
inference(forward_demodulation,[],[f1173,f1112]) ).
fof(f1191,plain,
! [X3,X1] : double_divide(double_divide(X3,identity),X1) = double_divide(identity,double_divide(double_divide(double_divide(double_divide(identity,identity),identity),X1),X3)),
inference(forward_demodulation,[],[f1175,f241]) ).
fof(f1195,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(double_divide(X1,double_divide(identity,double_divide(identity,double_divide(X0,double_divide(identity,identity))))),double_divide(identity,double_divide(double_divide(X0,identity),X2))),
inference(forward_demodulation,[],[f1180,f186]) ).
fof(f1199,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),double_divide(double_divide(double_divide(X2,identity),identity),identity)) = double_divide(identity,double_divide(X0,X2)),
inference(forward_demodulation,[],[f1189,f157]) ).
fof(f1200,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),X2) = double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),identity),X2),
inference(forward_demodulation,[],[f1190,f244]) ).
fof(f1201,plain,
! [X3,X1] : double_divide(double_divide(X3,identity),X1) = double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(identity,identity)),X1),X3)),
inference(forward_demodulation,[],[f1191,f157]) ).
fof(f1204,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(identity,double_divide(X0,double_divide(X2,double_divide(X1,double_divide(identity,double_divide(identity,double_divide(X0,double_divide(identity,identity)))))))),
inference(forward_demodulation,[],[f1195,f1185]) ).
fof(f1206,plain,
! [X2,X0] : double_divide(identity,double_divide(X0,X2)) = double_divide(double_divide(X2,identity),double_divide(identity,X0)),
inference(forward_demodulation,[],[f1199,f1072]) ).
fof(f1207,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),X2) = double_divide(double_divide(identity,double_divide(identity,double_divide(X0,double_divide(identity,identity)))),X2),
inference(forward_demodulation,[],[f1200,f157]) ).
fof(f1208,plain,
! [X3,X1] : double_divide(double_divide(X3,identity),X1) = double_divide(identity,double_divide(double_divide(identity,X1),X3)),
inference(forward_demodulation,[],[f1201,f7]) ).
fof(f1209,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(identity,double_divide(X0,double_divide(X2,double_divide(X1,double_divide(X0,double_divide(identity,identity)))))),
inference(forward_demodulation,[],[f1204,f244]) ).
fof(f1210,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),X2) = double_divide(double_divide(X0,double_divide(identity,identity)),X2),
inference(forward_demodulation,[],[f1207,f244]) ).
fof(f1211,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(identity,double_divide(X0,double_divide(X2,double_divide(X1,double_divide(identity,X0))))),
inference(forward_demodulation,[],[f1209,f186]) ).
fof(f1212,plain,
! [X2,X0] : double_divide(double_divide(X0,identity),X2) = double_divide(double_divide(identity,X0),X2),
inference(forward_demodulation,[],[f1210,f186]) ).
fof(f1213,plain,
! [X2,X1] : double_divide(double_divide(X1,identity),X2) = double_divide(identity,double_divide(double_divide(X2,identity),X1)),
inference(forward_demodulation,[],[f1211,f1093]) ).
fof(f1280,plain,
( double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) != double_divide(double_divide(a3,double_divide(identity,double_divide(c3,b3))),identity)
| a2 != double_divide(double_divide(a2,identity),identity)
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(superposition,[],[f8,f1114]) ).
fof(f1287,plain,
! [X2,X0,X1] : double_divide(double_divide(X2,double_divide(X0,double_divide(identity,X1))),double_divide(X0,identity)) = double_divide(double_divide(X2,identity),double_divide(X1,identity)),
inference(superposition,[],[f238,f1114]) ).
fof(f1290,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,identity)) = double_divide(X0,double_divide(identity,X1)),
inference(superposition,[],[f264,f1114]) ).
fof(f1322,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X2,X1)) = double_divide(double_divide(X2,double_divide(X0,double_divide(identity,X1))),double_divide(X0,identity)),
inference(forward_demodulation,[],[f1287,f1112]) ).
fof(f1329,plain,
( double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) != double_divide(double_divide(a3,double_divide(identity,double_divide(c3,b3))),identity)
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_subsumption_resolution,[],[f1280,f125]) ).
fof(f1386,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X2,X1)) = double_divide(double_divide(X0,identity),double_divide(X2,double_divide(X0,double_divide(identity,X1)))),
inference(forward_demodulation,[],[f1322,f264]) ).
fof(f1391,plain,
( double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) != double_divide(identity,double_divide(a3,double_divide(identity,double_divide(c3,b3))))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1329,f157]) ).
fof(f1432,plain,
! [X2,X1] : double_divide(identity,double_divide(X2,X1)) = double_divide(double_divide(X2,identity),double_divide(identity,X1)),
inference(forward_demodulation,[],[f1386,f212]) ).
fof(f1435,plain,
( double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) != double_divide(double_divide(a3,identity),double_divide(c3,b3))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1391,f1111]) ).
fof(f1465,plain,
( double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) != double_divide(double_divide(identity,a3),double_divide(c3,b3))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1435,f1212]) ).
fof(f1485,plain,
( double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) != double_divide(double_divide(identity,a3),double_divide(b3,c3))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1465,f264]) ).
fof(f1495,plain,
( double_divide(identity,double_divide(c3,double_divide(double_divide(b3,a3),identity))) != double_divide(double_divide(identity,a3),double_divide(b3,c3))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1485,f157]) ).
fof(f1501,plain,
( double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(c3,identity),double_divide(b3,a3))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1495,f1184]) ).
fof(f1505,plain,
( double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(b3,a3),double_divide(c3,identity))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1501,f264]) ).
fof(f1508,plain,
( double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(b3,a3),double_divide(identity,c3))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1505,f1290]) ).
fof(f1510,plain,
( double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,c3),double_divide(b3,a3))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1508,f264]) ).
fof(f1512,plain,
( double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,c3),double_divide(a3,b3))
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity)
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1510,f264]) ).
fof(f1513,plain,
( identity != double_divide(identity,double_divide(a1,double_divide(a1,identity)))
| double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,c3),double_divide(a3,b3))
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1512,f157]) ).
fof(f1514,plain,
( identity != double_divide(double_divide(a1,identity),a1)
| double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,c3),double_divide(a3,b3))
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_demodulation,[],[f1513,f1184]) ).
fof(f1515,plain,
( double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,c3),double_divide(a3,b3))
| double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity) ),
inference(forward_subsumption_resolution,[],[f1514,f128]) ).
fof(f1516,plain,
( double_divide(double_divide(b4,a4),identity) != double_divide(identity,double_divide(a4,b4))
| double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,c3),double_divide(a3,b3)) ),
inference(forward_demodulation,[],[f1515,f157]) ).
fof(f1517,plain,
( double_divide(identity,double_divide(a4,b4)) != double_divide(identity,double_divide(b4,a4))
| double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,c3),double_divide(a3,b3)) ),
inference(forward_demodulation,[],[f1516,f157]) ).
fof(f1518,plain,
( double_divide(identity,double_divide(a4,b4)) != double_divide(identity,double_divide(a4,b4))
| double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,c3),double_divide(a3,b3)) ),
inference(forward_demodulation,[],[f1517,f264]) ).
fof(f1519,plain,
double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,c3),double_divide(a3,b3)),
inference(trivial_inequality_removal,[],[f1518]) ).
fof(f1735,plain,
! [X0,X1] : double_divide(X1,double_divide(X0,identity)) = double_divide(double_divide(identity,X0),X1),
inference(superposition,[],[f264,f1212]) ).
fof(f2245,plain,
! [X2,X0,X1] : double_divide(double_divide(X2,identity),double_divide(double_divide(X0,identity),X1)) = double_divide(identity,double_divide(double_divide(X0,double_divide(X1,identity)),X2)),
inference(superposition,[],[f1206,f1184]) ).
fof(f2281,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X1,X2)) = double_divide(identity,double_divide(double_divide(X0,double_divide(X1,identity)),X2)),
inference(forward_demodulation,[],[f2245,f1072]) ).
fof(f2416,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),identity) = double_divide(identity,double_divide(X1,X0)),
inference(superposition,[],[f207,f113]) ).
fof(f2507,plain,
! [X0,X1] : double_divide(identity,double_divide(X0,X1)) = double_divide(identity,double_divide(X1,X0)),
inference(forward_demodulation,[],[f2416,f157]) ).
fof(f2702,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(X1,X0),X2)) = double_divide(double_divide(X2,identity),double_divide(identity,double_divide(X0,X1))),
inference(superposition,[],[f1206,f2507]) ).
fof(f2746,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(X0,X1),X2)) = double_divide(identity,double_divide(double_divide(X1,X0),X2)),
inference(forward_demodulation,[],[f2702,f1206]) ).
fof(f3501,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(X0,identity),X1),X2)) = double_divide(double_divide(X2,identity),double_divide(double_divide(X1,identity),X0)),
inference(superposition,[],[f1208,f1213]) ).
fof(f3502,plain,
! [X2,X0,X1] : double_divide(X2,double_divide(double_divide(X0,identity),X1)) = double_divide(double_divide(double_divide(double_divide(X1,identity),X0),identity),X2),
inference(superposition,[],[f1114,f1213]) ).
fof(f3534,plain,
! [X2,X0,X1] : double_divide(X2,double_divide(double_divide(X0,identity),X1)) = double_divide(double_divide(identity,double_divide(double_divide(X1,identity),X0)),X2),
inference(forward_demodulation,[],[f3502,f1212]) ).
fof(f3535,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,X2)) = double_divide(identity,double_divide(double_divide(double_divide(X0,identity),X1),X2)),
inference(forward_demodulation,[],[f3501,f1072]) ).
fof(f3569,plain,
! [X2,X0,X1] : double_divide(X2,double_divide(double_divide(X0,identity),X1)) = double_divide(double_divide(identity,identity),double_divide(X1,double_divide(X0,X2))),
inference(forward_demodulation,[],[f3534,f1174]) ).
fof(f3597,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,double_divide(X0,X2)),identity) = double_divide(X2,double_divide(double_divide(X0,identity),X1)),
inference(forward_demodulation,[],[f3569,f123]) ).
fof(f3617,plain,
! [X2,X0,X1] : double_divide(X2,double_divide(double_divide(X0,identity),X1)) = double_divide(identity,double_divide(X1,double_divide(X0,X2))),
inference(forward_demodulation,[],[f3597,f157]) ).
fof(f3670,plain,
! [X2,X0,X1] : double_divide(double_divide(X2,identity),double_divide(double_divide(X0,identity),X1)) = double_divide(identity,double_divide(X2,double_divide(double_divide(X1,identity),X0))),
inference(superposition,[],[f1432,f1213]) ).
fof(f3674,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(double_divide(X0,double_divide(identity,X2)),double_divide(X2,identity)))) = double_divide(double_divide(X1,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity))),
inference(superposition,[],[f1432,f10]) ).
fof(f3746,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(double_divide(X0,double_divide(identity,X2)),double_divide(X2,identity)))) = double_divide(identity,double_divide(double_divide(double_divide(X1,identity),identity),double_divide(identity,double_divide(X0,double_divide(identity,identity))))),
inference(forward_demodulation,[],[f3674,f241]) ).
fof(f3749,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(X0,double_divide(X2,identity)))) = double_divide(identity,double_divide(X2,double_divide(double_divide(X1,identity),X0))),
inference(forward_demodulation,[],[f3670,f3617]) ).
fof(f3777,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(double_divide(X0,double_divide(identity,X2)),double_divide(X2,identity)))) = double_divide(double_divide(double_divide(double_divide(X1,identity),identity),identity),double_divide(X0,double_divide(identity,identity))),
inference(forward_demodulation,[],[f3746,f1111]) ).
fof(f3778,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,X2),X0) = double_divide(identity,double_divide(X2,double_divide(double_divide(X1,identity),X0))),
inference(forward_demodulation,[],[f3749,f195]) ).
fof(f3795,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(double_divide(X0,double_divide(identity,X2)),double_divide(X2,identity)))) = double_divide(identity,double_divide(double_divide(double_divide(double_divide(double_divide(X1,identity),identity),identity),identity),X0)),
inference(forward_demodulation,[],[f3777,f241]) ).
fof(f3809,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(double_divide(X0,double_divide(identity,X2)),double_divide(X2,identity)))) = double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(double_divide(X1,identity),identity),identity)),X0)),
inference(forward_demodulation,[],[f3795,f2746]) ).
fof(f3818,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(double_divide(double_divide(X1,identity),identity),identity)) = double_divide(identity,double_divide(X1,double_divide(double_divide(X0,double_divide(identity,X2)),double_divide(X2,identity)))),
inference(forward_demodulation,[],[f3809,f1208]) ).
fof(f3823,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,identity),double_divide(double_divide(double_divide(X1,identity),identity),identity)) = double_divide(double_divide(X1,X2),double_divide(X0,double_divide(identity,X2))),
inference(forward_demodulation,[],[f3818,f195]) ).
fof(f3828,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,X2),double_divide(X0,double_divide(identity,X2))) = double_divide(identity,double_divide(identity,double_divide(double_divide(X1,identity),double_divide(X0,identity)))),
inference(forward_demodulation,[],[f3823,f3617]) ).
fof(f3833,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),double_divide(X0,identity)) = double_divide(double_divide(X1,X2),double_divide(X0,double_divide(identity,X2))),
inference(forward_demodulation,[],[f3828,f244]) ).
fof(f3837,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(X1,X2),double_divide(X0,double_divide(identity,X2))),
inference(forward_demodulation,[],[f3833,f1112]) ).
fof(f3876,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(double_divide(X0,double_divide(X1,X3)),double_divide(X3,identity))) = double_divide(double_divide(X1,identity),double_divide(X2,double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)))),
inference(superposition,[],[f212,f10]) ).
fof(f3881,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X0,double_divide(X2,X1))) = double_divide(double_divide(double_divide(X2,identity),identity),double_divide(X3,double_divide(double_divide(X0,identity),X1))),
inference(superposition,[],[f212,f212]) ).
fof(f3951,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X2,X1)),identity) = double_divide(identity,double_divide(double_divide(X2,identity),double_divide(double_divide(X0,identity),X1))),
inference(superposition,[],[f207,f212]) ).
fof(f3956,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X2,X1)),identity) = double_divide(double_divide(X0,double_divide(X2,identity)),X1),
inference(forward_demodulation,[],[f3951,f3778]) ).
fof(f4011,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X0,double_divide(X2,X1))) = double_divide(double_divide(identity,double_divide(X2,identity)),double_divide(X3,double_divide(double_divide(X0,identity),X1))),
inference(forward_demodulation,[],[f3881,f1212]) ).
fof(f4016,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(double_divide(X0,double_divide(X1,X3)),double_divide(X3,identity))) = double_divide(double_divide(X1,identity),double_divide(X2,double_divide(double_divide(identity,identity),double_divide(identity,double_divide(X0,double_divide(identity,identity)))))),
inference(forward_demodulation,[],[f3876,f1735]) ).
fof(f4035,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X2,identity)),X1) = double_divide(identity,double_divide(X0,double_divide(X2,X1))),
inference(forward_demodulation,[],[f3956,f157]) ).
fof(f4080,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X0,double_divide(X2,X1))) = double_divide(X2,double_divide(X3,double_divide(double_divide(X0,identity),X1))),
inference(forward_demodulation,[],[f4011,f113]) ).
fof(f4084,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(double_divide(X0,double_divide(X1,X3)),double_divide(X3,identity))) = double_divide(double_divide(X1,identity),double_divide(X2,double_divide(identity,double_divide(double_divide(X0,double_divide(identity,identity)),identity)))),
inference(forward_demodulation,[],[f4016,f1206]) ).
fof(f4137,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(double_divide(X0,double_divide(X1,X3)),double_divide(X3,identity))) = double_divide(identity,double_divide(X1,double_divide(double_divide(X2,identity),double_divide(double_divide(X0,double_divide(identity,identity)),identity)))),
inference(forward_demodulation,[],[f4084,f4080]) ).
fof(f4171,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(double_divide(X0,double_divide(X1,X3)),double_divide(X3,identity))) = double_divide(double_divide(X2,X1),double_divide(double_divide(X0,double_divide(identity,identity)),identity)),
inference(forward_demodulation,[],[f4137,f3778]) ).
fof(f4193,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,identity),double_divide(double_divide(X0,double_divide(X1,X3)),double_divide(X3,identity))) = double_divide(double_divide(X2,X1),double_divide(identity,double_divide(X0,double_divide(identity,identity)))),
inference(forward_demodulation,[],[f4171,f1290]) ).
fof(f4210,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,X1),X0) = double_divide(double_divide(X2,identity),double_divide(double_divide(X0,double_divide(X1,X3)),double_divide(X3,identity))),
inference(forward_demodulation,[],[f4193,f152]) ).
fof(f4221,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,X1),X0) = double_divide(identity,double_divide(double_divide(double_divide(X2,identity),X3),double_divide(X0,double_divide(X1,X3)))),
inference(forward_demodulation,[],[f4210,f241]) ).
fof(f4230,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,X1),X0) = double_divide(X3,double_divide(X2,double_divide(X0,double_divide(X1,X3)))),
inference(forward_demodulation,[],[f4221,f3535]) ).
fof(f4695,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X2,double_divide(identity,X1))) = double_divide(identity,double_divide(double_divide(X1,X0),X2)),
inference(superposition,[],[f3837,f128]) ).
fof(f4727,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(X0,double_divide(X1,identity)),X2)) = double_divide(X0,double_divide(X2,double_divide(identity,double_divide(X1,identity)))),
inference(superposition,[],[f3837,f206]) ).
fof(f4826,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X1,double_divide(identity,X2))) = double_divide(double_divide(double_divide(X0,X2),identity),double_divide(X3,double_divide(identity,double_divide(X0,X1)))),
inference(superposition,[],[f212,f3837]) ).
fof(f4836,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X1,double_divide(identity,X2))) = double_divide(identity,double_divide(double_divide(X0,X2),double_divide(double_divide(X3,identity),double_divide(X0,X1)))),
inference(forward_demodulation,[],[f4826,f4080]) ).
fof(f4898,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X2,X1)) = double_divide(identity,double_divide(double_divide(X0,double_divide(X1,identity)),X2)),
inference(forward_demodulation,[],[f4727,f113]) ).
fof(f4928,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X1,double_divide(identity,X2))) = double_divide(double_divide(X3,double_divide(X0,X2)),double_divide(X0,X1)),
inference(forward_demodulation,[],[f4836,f3778]) ).
fof(f4973,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X2,X1)) = double_divide(identity,double_divide(identity,double_divide(X0,double_divide(X1,X2)))),
inference(forward_demodulation,[],[f4898,f4035]) ).
fof(f4988,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,double_divide(X0,X2)),double_divide(X0,X1)) = double_divide(identity,double_divide(double_divide(X2,double_divide(X3,identity)),X1)),
inference(forward_demodulation,[],[f4928,f4695]) ).
fof(f5019,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X1,X2)) = double_divide(X0,double_divide(X2,X1)),
inference(forward_demodulation,[],[f4973,f244]) ).
fof(f5028,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(X3,X1)) = double_divide(double_divide(X3,double_divide(X0,X2)),double_divide(X0,X1)),
inference(forward_demodulation,[],[f4988,f2281]) ).
fof(f5310,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X1,X2)) = double_divide(double_divide(X2,X1),X0),
inference(superposition,[],[f264,f5019]) ).
fof(f5331,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,X0),double_divide(X1,X2)) = double_divide(double_divide(X0,identity),double_divide(X2,X1)),
inference(superposition,[],[f1212,f5019]) ).
fof(f5810,plain,
! [X2,X3,X0,X1] : double_divide(X3,double_divide(double_divide(X0,X1),X2)) = double_divide(X3,double_divide(double_divide(X1,X0),X2)),
inference(superposition,[],[f5019,f5310]) ).
fof(f9269,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,identity),double_divide(X2,X0)) = double_divide(double_divide(X1,X2),double_divide(X0,identity)),
inference(superposition,[],[f1124,f207]) ).
fof(f9933,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(double_divide(X0,identity),double_divide(X1,X2)),double_divide(X3,identity)) = double_divide(double_divide(double_divide(X0,X1),identity),double_divide(double_divide(X2,identity),X3)),
inference(superposition,[],[f9269,f9269]) ).
fof(f10024,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X1,X2)) = double_divide(double_divide(double_divide(X0,identity),identity),double_divide(X3,double_divide(double_divide(X0,X1),double_divide(X2,identity)))),
inference(superposition,[],[f212,f9269]) ).
fof(f10174,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X1,X2)) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(double_divide(double_divide(X0,X1),double_divide(X2,identity)),X3)),
inference(forward_demodulation,[],[f10024,f5331]) ).
fof(f10225,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(double_divide(X0,identity),double_divide(X1,X2)),double_divide(X3,identity)) = double_divide(identity,double_divide(X3,double_divide(X2,double_divide(double_divide(X0,X1),identity)))),
inference(forward_demodulation,[],[f9933,f3617]) ).
fof(f10339,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X1,X2)) = double_divide(identity,double_divide(identity,double_divide(X0,double_divide(double_divide(double_divide(X0,X1),double_divide(X2,identity)),X3)))),
inference(forward_demodulation,[],[f10174,f4035]) ).
fof(f10374,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(double_divide(X0,identity),double_divide(X1,X2)),double_divide(X3,identity)) = double_divide(double_divide(X3,double_divide(X0,X1)),X2),
inference(forward_demodulation,[],[f10225,f4230]) ).
fof(f10465,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X1,X2)) = double_divide(X0,double_divide(double_divide(double_divide(X0,X1),double_divide(X2,identity)),X3)),
inference(forward_demodulation,[],[f10339,f244]) ).
fof(f10495,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,double_divide(X0,X1)),X2) = double_divide(double_divide(double_divide(X0,identity),identity),double_divide(X3,double_divide(X1,X2))),
inference(forward_demodulation,[],[f10374,f1017]) ).
fof(f10569,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,identity),double_divide(X1,X2)) = double_divide(X0,double_divide(identity,double_divide(double_divide(X0,X1),double_divide(X2,X3)))),
inference(forward_demodulation,[],[f10465,f4035]) ).
fof(f10588,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,double_divide(X0,X1)),X2) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(double_divide(X1,X2),X3)),
inference(forward_demodulation,[],[f10495,f5331]) ).
fof(f10639,plain,
! [X2,X3,X1] : double_divide(double_divide(X3,identity),double_divide(X1,X2)) = double_divide(double_divide(X2,X3),double_divide(X1,identity)),
inference(forward_demodulation,[],[f10569,f1142]) ).
fof(f10653,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,double_divide(X0,X1)),X2) = double_divide(identity,double_divide(identity,double_divide(X0,double_divide(double_divide(X1,X2),X3)))),
inference(forward_demodulation,[],[f10588,f4035]) ).
fof(f10700,plain,
! [X2,X3,X0,X1] : double_divide(X0,double_divide(double_divide(X1,X2),X3)) = double_divide(double_divide(X3,double_divide(X0,X1)),X2),
inference(forward_demodulation,[],[f10653,f244]) ).
fof(f10871,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X0,double_divide(identity,X1)),double_divide(X3,identity)) = double_divide(double_divide(double_divide(X1,double_divide(X0,X2)),identity),double_divide(X3,double_divide(X2,identity))),
inference(superposition,[],[f10639,f312]) ).
fof(f11201,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X0,double_divide(identity,X1)),double_divide(X3,identity)) = double_divide(identity,double_divide(double_divide(double_divide(double_divide(X1,double_divide(X0,X2)),identity),X2),X3)),
inference(forward_demodulation,[],[f10871,f241]) ).
fof(f11344,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X0,double_divide(identity,X1)),double_divide(X3,identity)) = double_divide(identity,double_divide(double_divide(X2,double_divide(double_divide(X1,double_divide(X0,X2)),identity)),X3)),
inference(forward_demodulation,[],[f11201,f5810]) ).
fof(f11457,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(double_divide(X1,double_divide(X0,X2)),X3)) = double_divide(double_divide(X0,double_divide(identity,X1)),double_divide(X3,identity)),
inference(forward_demodulation,[],[f11344,f2281]) ).
fof(f11548,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(double_divide(X1,double_divide(X0,X2)),X3)) = double_divide(identity,double_divide(double_divide(X1,double_divide(X3,identity)),X0)),
inference(forward_demodulation,[],[f11457,f10700]) ).
fof(f11627,plain,
! [X2,X3,X0,X1] : double_divide(X1,double_divide(X3,X0)) = double_divide(X2,double_divide(double_divide(X1,double_divide(X0,X2)),X3)),
inference(forward_demodulation,[],[f11548,f2281]) ).
fof(f11686,plain,
! [X2,X3,X0,X1] : double_divide(X1,double_divide(X3,X0)) = double_divide(X2,double_divide(X0,double_divide(double_divide(X2,X3),X1))),
inference(forward_demodulation,[],[f11627,f10700]) ).
fof(f16257,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(X1,X2),double_divide(X3,X4)) = double_divide(double_divide(X3,double_divide(double_divide(X0,X1),double_divide(X2,identity))),double_divide(double_divide(X0,identity),X4)),
inference(superposition,[],[f5028,f9269]) ).
fof(f16346,plain,
! [X2,X3,X0,X1] : double_divide(X1,double_divide(X2,X3)) = double_divide(double_divide(X2,double_divide(double_divide(X3,X0),X1)),X0),
inference(superposition,[],[f5028,f128]) ).
fof(f16658,plain,
! [X2,X3,X0,X1] : double_divide(X1,double_divide(X2,X3)) = double_divide(X0,double_divide(X2,double_divide(double_divide(X3,X0),X1))),
inference(forward_demodulation,[],[f16346,f264]) ).
fof(f16740,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(X1,X2),double_divide(X3,X4)) = double_divide(identity,double_divide(X4,double_divide(X0,double_divide(X3,double_divide(double_divide(X0,X1),double_divide(X2,identity)))))),
inference(forward_demodulation,[],[f16257,f3617]) ).
fof(f16932,plain,
! [X2,X3,X1,X4] : double_divide(double_divide(X1,X2),double_divide(X3,X4)) = double_divide(identity,double_divide(X4,double_divide(double_divide(X2,identity),double_divide(X1,X3)))),
inference(forward_demodulation,[],[f16740,f11686]) ).
fof(f17064,plain,
! [X2,X3,X1,X4] : double_divide(double_divide(X1,X2),double_divide(X3,X4)) = double_divide(double_divide(X1,X3),double_divide(X4,X2)),
inference(forward_demodulation,[],[f16932,f16658]) ).
fof(f17712,plain,
double_divide(double_divide(identity,a3),double_divide(b3,c3)) != double_divide(double_divide(identity,a3),double_divide(b3,c3)),
inference(superposition,[],[f1519,f17064]) ).
fof(f17878,plain,
$false,
inference(trivial_inequality_removal,[],[f17712]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP100-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 09:19:50 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.89/2.01 % (3124262)Input is clausal, will run a generic CNF schedule.
% 6.89/2.01 % (3124271)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=936534897:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.89/2.01 % (3124268)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=299797217:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.89/2.01 % (3124271)Instruction limit reached!
% 6.89/2.01 % (3124271)------------------------------
% 6.89/2.01 % (3124271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124271)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124271)Termination reason: Instruction limit
% 6.89/2.01 % (3124271)Termination phase: Saturation
% 6.89/2.01 % (3124271)Time elapsed: 0.038 s
% 6.89/2.01 % (3124271)Peak memory usage: 89 MB
% 6.89/2.01 % (3124271)Instructions burned: 114 (million)
% 6.89/2.01 % (3124273)dis-21_1_sil=8000:lcm=predicate:random_seed=2699614956:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.89/2.01 % (3124267)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=963499890:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.89/2.01 % (3124269)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3844776934:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.89/2.01 % (3124273)Refutation not found, incomplete strategy
% 6.89/2.01 % (3124273)------------------------------
% 6.89/2.01 % (3124273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124273)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124273)Termination reason: Refutation not found, incomplete strategy
% 6.89/2.01 % (3124273)Time elapsed: 0.001 s
% 6.89/2.01 % (3124273)Peak memory usage: 88 MB
% 6.89/2.01 % (3124270)lrs+10_1_sil=8000:sp=occurrence:random_seed=2124701949:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.89/2.01 % (3124272)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=361310207:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.89/2.01 % (3124270)Instruction limit reached!
% 6.89/2.01 % (3124270)------------------------------
% 6.89/2.01 % (3124270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124270)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124270)Termination reason: Instruction limit
% 6.89/2.01 % (3124270)Termination phase: Saturation
% 6.89/2.01 % (3124270)Time elapsed: 0.066 s
% 6.89/2.01 % (3124270)Peak memory usage: 89 MB
% 6.89/2.01 % (3124270)Instructions burned: 107 (million)
% 6.89/2.01 % (3124279)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2537663787:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.89/2.01 % (3124279)Refutation not found, incomplete strategy
% 6.89/2.01 % (3124279)------------------------------
% 6.89/2.01 % (3124279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124279)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124279)Termination reason: Refutation not found, incomplete strategy
% 6.89/2.01 % (3124279)Time elapsed: 0.001 s
% 6.89/2.01 % (3124279)Peak memory usage: 88 MB
% 6.89/2.01 % (3124272)Instruction limit reached!
% 6.89/2.01 % (3124272)------------------------------
% 6.89/2.01 % (3124272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124272)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124272)Termination reason: Instruction limit
% 6.89/2.01 % (3124272)Termination phase: Saturation
% 6.89/2.01 % (3124272)Time elapsed: 0.105 s
% 6.89/2.01 % (3124272)Peak memory usage: 90 MB
% 6.89/2.01 % (3124272)Instructions burned: 180 (million)
% 6.89/2.01 % (3124282)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3858611656:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 6.89/2.01 % (3124282)Refutation not found, incomplete strategy
% 6.89/2.01 % (3124282)------------------------------
% 6.89/2.01 % (3124282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124282)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124282)Termination reason: Refutation not found, incomplete strategy
% 6.89/2.01 % (3124282)Time elapsed: 0.001 s
% 6.89/2.01 % (3124282)Peak memory usage: 88 MB
% 6.89/2.01 % (3124279)------------------------------
% 6.89/2.01 % (3124279)------------------------------
% 6.89/2.01 % (3124273)------------------------------
% 6.89/2.01 % (3124273)------------------------------
% 6.89/2.01 % (3124284)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=74611188:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 6.89/2.01 % (3124284)Refutation not found, incomplete strategy
% 6.89/2.01 % (3124284)------------------------------
% 6.89/2.01 % (3124284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124284)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124284)Termination reason: Refutation not found, incomplete strategy
% 6.89/2.01 % (3124284)Time elapsed: 0.001 s
% 6.89/2.01 % (3124284)Peak memory usage: 88 MB
% 6.89/2.01 % (3124284)Instructions burned: 1 (million)
% 6.89/2.01 % (3124286)lrs+10_64_to=lpo:sil=8000:random_seed=2100942623:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 6.89/2.01 % (3124288)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4089241661:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 6.89/2.01 % (3124286)Instruction limit reached!
% 6.89/2.01 % (3124286)------------------------------
% 6.89/2.01 % (3124286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124286)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124286)Termination reason: Instruction limit
% 6.89/2.01 % (3124286)Termination phase: Saturation
% 6.89/2.01 % (3124286)Time elapsed: 0.076 s
% 6.89/2.01 % (3124286)Peak memory usage: 88 MB
% 6.89/2.01 % (3124286)Instructions burned: 127 (million)
% 6.89/2.01 % (3124282)------------------------------
% 6.89/2.01 % (3124282)------------------------------
% 6.89/2.01 % (3124288)Instruction limit reached!
% 6.89/2.01 % (3124288)------------------------------
% 6.89/2.01 % (3124288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124288)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124288)Termination reason: Instruction limit
% 6.89/2.01 % (3124288)Termination phase: Saturation
% 6.89/2.01 % (3124288)Time elapsed: 0.114 s
% 6.89/2.01 % (3124288)Peak memory usage: 89 MB
% 6.89/2.01 % (3124288)Instructions burned: 195 (million)
% 6.89/2.01 % (3124284)------------------------------
% 6.89/2.01 % (3124284)------------------------------
% 6.89/2.01 % (3124291)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2120184234:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 6.89/2.01 % (3124292)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3401246849:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 6.89/2.01 % (3124294)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1660853754:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 6.89/2.01 % (3124293)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3183822806:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 6.89/2.01 % (3124294)Refutation not found, incomplete strategy
% 6.89/2.01 % (3124294)------------------------------
% 6.89/2.01 % (3124294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124294)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124294)Termination reason: Refutation not found, incomplete strategy
% 6.89/2.01 % (3124294)Time elapsed: 0.001 s
% 6.89/2.01 % (3124294)Peak memory usage: 88 MB
% 6.89/2.01 % (3124291)Instruction limit reached!
% 6.89/2.01 % (3124291)------------------------------
% 6.89/2.01 % (3124291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124291)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124291)Termination reason: Instruction limit
% 6.89/2.01 % (3124291)Termination phase: Saturation
% 6.89/2.01 % (3124291)Time elapsed: 0.088 s
% 6.89/2.01 % (3124291)Peak memory usage: 91 MB
% 6.89/2.01 % (3124291)Instructions burned: 158 (million)
% 6.89/2.01 % (3124293)Instruction limit reached!
% 6.89/2.01 % (3124293)------------------------------
% 6.89/2.01 % (3124293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124293)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124293)Termination reason: Instruction limit
% 6.89/2.01 % (3124293)Termination phase: Saturation
% 6.89/2.01 % (3124293)Time elapsed: 0.066 s
% 6.89/2.01 % (3124293)Peak memory usage: 89 MB
% 6.89/2.01 % (3124293)Instructions burned: 106 (million)
% 6.89/2.01 % (3124299)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2926611125:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 6.89/2.01 % (3124300)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4153528006:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 6.89/2.01 % (3124268)First to succeed.
% 6.89/2.01 % (3124294)------------------------------
% 6.89/2.01 % (3124294)------------------------------
% 6.89/2.01 % (3124268)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3124262"
% 6.89/2.01 % (3124269)Also succeeded, but the first one will report.
% 6.89/2.01 % (3124299)Instruction limit reached!
% 6.89/2.01 % (3124299)------------------------------
% 6.89/2.01 % (3124299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.89/2.01 % (3124299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.89/2.01 % (3124299)CaDiCaL version: 2.1.3
% 6.89/2.01 % (3124299)Termination reason: Instruction limit
% 6.89/2.01 % (3124299)Termination phase: Saturation
% 6.89/2.01 % (3124299)Time elapsed: 0.134 s
% 6.89/2.01 % (3124299)Peak memory usage: 91 MB
% 6.89/2.01 % (3124299)Instructions burned: 243 (million)
% 6.89/2.01 % (3124303)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1393481963:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 6.89/2.01 % (3124268)Refutation found. Thanks to Tanya!
% 6.89/2.01 % SZS status Unsatisfiable for theBenchmark
% 6.89/2.01 % SZS output start Proof for theBenchmark
% See solution above
% 8.67/2.11 % (3124268)------------------------------
% 8.67/2.11 % (3124268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.11 % (3124268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.11 % (3124268)CaDiCaL version: 2.1.3
% 8.67/2.11 % (3124268)Termination reason: Refutation
% 8.67/2.11 % (3124268)Time elapsed: 0.860 s
% 8.67/2.11 % (3124268)Peak memory usage: 135 MB
% 8.67/2.11 % (3124268)Instructions burned: 1787 (million)
% 8.67/2.11 % (3124268)------------------------------
% 8.67/2.11 % (3124268)------------------------------
% 8.67/2.11 % (3124262)Success in time 1.163 s
% 8.67/2.11 % Vampire exiting
%------------------------------------------------------------------------------