%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO074-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:06:39 PM UTC 2026
% Result : Unsatisfiable 103.78s 13.67s
% Output : CNFRefutation 103.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 2
% Syntax : Number of formulae : 91 ( 91 unt; 0 def)
% Number of atoms : 91 ( 90 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 25 ( 4 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 218 ( 218 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : inverse(add(inverse(add(inverse(add(A,B)),C)),inverse(add(A,inverse(add(inverse(C),inverse(add(C,D)))))))) = C,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
add(inverse(add(inverse(a),b)),inverse(add(inverse(a),inverse(b)))) != a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2,X3] : inverse(add(inverse(add(inverse(add(X0,X1)),X2)),inverse(add(X0,inverse(add(inverse(X2),inverse(add(X2,X3)))))))) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
add(inverse(add(inverse(a),b)),inverse(add(inverse(a),inverse(b)))) != a,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f13,plain,
! [X0,X1,X2,X3,X4] : inverse(add(X0,inverse(add(inverse(add(X1,X2)),inverse(add(inverse(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X3))))))),inverse(add(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X3)))))),X4)))))))) = inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X3)))))),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f15,plain,
! [X0,X1,X2] : inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(X0)),X1)),X0)),X2)),inverse(X0))),X0)) = inverse(X0),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f18,plain,
! [X0] : inverse(add(inverse(add(X0,inverse(X0))),X0)) = inverse(X0),
inference(paramodulation,[status(thm)],[f3,f15]) ).
fof(f39,plain,
! [X0,X1] : inverse(add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1)))))))) = X0,
inference(paramodulation,[status(thm)],[f18,f3]) ).
fof(f57,plain,
! [X0] : inverse(add(inverse(X0),inverse(add(X0,X0)))) = X0,
inference(paramodulation,[status(thm)],[f39,f39]) ).
fof(f69,plain,
! [X0,X1,X2] : inverse(add(inverse(add(inverse(add(X0,X1)),X2)),inverse(add(X0,X2)))) = X2,
inference(paramodulation,[status(thm)],[f39,f3]) ).
fof(f97,plain,
! [X0,X1,X2] : inverse(add(add(X0,X1),inverse(add(X0,inverse(add(inverse(inverse(add(add(X0,X1),add(X0,X1)))),inverse(add(inverse(add(add(X0,X1),add(X0,X1))),X2)))))))) = inverse(add(add(X0,X1),add(X0,X1))),
inference(paramodulation,[status(thm)],[f57,f3]) ).
fof(f122,plain,
! [X0,X1,X2,X3] : inverse(add(X0,inverse(add(inverse(add(X1,X2)),inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X3)))))))))) = inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X3)))))),
inference(paramodulation,[status(thm)],[f39,f13]) ).
fof(f125,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X5)))))))) = inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),inverse(add(inverse(X0),inverse(add(X0,X1)))))),
inference(paramodulation,[status(thm)],[f15,f13]) ).
fof(f170,plain,
! [X0,X1,X2] : inverse(add(inverse(inverse(add(X0,X1))),inverse(add(inverse(add(X0,X1)),inverse(add(X0,inverse(add(inverse(inverse(inverse(add(X0,X1)))),inverse(add(inverse(inverse(add(X0,X1))),X2)))))))))) = inverse(add(X0,X1)),
inference(paramodulation,[status(thm)],[f13,f39]) ).
fof(f183,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5)))))))) = inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),inverse(add(inverse(X0),inverse(add(X0,X1)))))),
inference(forward_demodulation,[status(thm)],[f15,f125]) ).
fof(f184,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5)))))))) = inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),
inference(forward_demodulation,[status(thm)],[f15,f183]) ).
fof(f259,plain,
! [X0,X1,X2] : inverse(add(X0,inverse(add(inverse(inverse(inverse(add(X0,X1)))),inverse(add(inverse(inverse(add(X0,X1))),X2)))))) = inverse(add(X0,X1)),
inference(forward_demodulation,[status(thm)],[f122,f170]) ).
fof(f274,plain,
! [X0,X1,X2] : inverse(add(add(X0,X1),inverse(add(X0,inverse(add(add(X0,X1),inverse(add(inverse(add(X0,X1)),inverse(add(add(X0,X1),X2)))))))))) = inverse(add(add(X0,X1),inverse(add(inverse(add(X0,X1)),inverse(add(add(X0,X1),X2)))))),
inference(paramodulation,[status(thm)],[f39,f69]) ).
fof(f281,plain,
! [X0,X1] : inverse(add(inverse(add(X0,X1)),inverse(add(inverse(X0),X1)))) = X1,
inference(paramodulation,[status(thm)],[f39,f69]) ).
fof(f343,plain,
! [X0] : inverse(add(inverse(add(add(X0,inverse(X0)),X0)),inverse(X0))) = X0,
inference(paramodulation,[status(thm)],[f18,f281]) ).
fof(f346,plain,
! [X0] : inverse(add(inverse(add(X0,inverse(add(X0,X0)))),X0)) = inverse(add(X0,X0)),
inference(paramodulation,[status(thm)],[f57,f281]) ).
fof(f358,plain,
! [X0,X1] : inverse(add(X0,inverse(add(X1,inverse(add(inverse(X1),X0)))))) = inverse(add(inverse(X1),X0)),
inference(paramodulation,[status(thm)],[f281,f69]) ).
fof(f432,plain,
! [X0] : inverse(add(X0,inverse(add(add(X0,inverse(X0)),inverse(X0))))) = inverse(X0),
inference(paramodulation,[status(thm)],[f343,f69]) ).
fof(f522,plain,
! [X0,X1] : inverse(add(inverse(add(inverse(X0),X1)),inverse(add(X0,X1)))) = X1,
inference(paramodulation,[status(thm)],[f432,f69]) ).
fof(f525,plain,
! [X0,X1,X2,X3] : inverse(add(X0,inverse(add(inverse(X1),inverse(add(inverse(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2))))))),inverse(add(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2)))))),X3)))))))) = inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2)))))),
inference(paramodulation,[status(thm)],[f432,f13]) ).
fof(f526,plain,
! [X0] : inverse(add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(X0))))))) = X0,
inference(paramodulation,[status(thm)],[f432,f39]) ).
fof(f587,plain,
! [X0] : inverse(add(inverse(X0),inverse(X0))) = X0,
inference(forward_demodulation,[status(thm)],[f358,f526]) ).
fof(f607,plain,
! [X0,X1,X2] : inverse(add(X0,inverse(add(inverse(add(inverse(add(X1,X2)),X0)),inverse(add(X1,X0)))))) = add(inverse(add(inverse(add(X1,X2)),X0)),inverse(add(X1,X0))),
inference(paramodulation,[status(thm)],[f69,f587]) ).
fof(f609,plain,
! [X0,X1] : inverse(add(X0,inverse(add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0)))))) = add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))),
inference(paramodulation,[status(thm)],[f281,f587]) ).
fof(f610,plain,
! [X0,X1] : inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1)))))))))) = add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))),
inference(paramodulation,[status(thm)],[f39,f587]) ).
fof(f612,plain,
! [X0] : inverse(add(X0,inverse(add(inverse(X0),inverse(X0))))) = add(inverse(X0),inverse(X0)),
inference(paramodulation,[status(thm)],[f587,f587]) ).
fof(f637,plain,
! [X0,X1] : inverse(add(inverse(add(X0,X1)),inverse(add(inverse(X0),X1)))) = X1,
inference(paramodulation,[status(thm)],[f587,f69]) ).
fof(f703,plain,
! [X0,X1,X2] : inverse(add(X0,X0)) = add(inverse(add(inverse(add(X1,X2)),X0)),inverse(add(X1,X0))),
inference(forward_demodulation,[status(thm)],[f69,f607]) ).
fof(f726,plain,
! [X0,X1] : inverse(add(X0,X0)) = add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))),
inference(forward_demodulation,[status(thm)],[f281,f609]) ).
fof(f737,plain,
! [X0,X1] : inverse(add(X0,X0)) = add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))),
inference(forward_demodulation,[status(thm)],[f39,f610]) ).
fof(f750,plain,
! [X0] : inverse(add(X0,X0)) = add(inverse(X0),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f587,f612]) ).
fof(f794,plain,
! [X0,X1,X2] : inverse(add(add(X0,X1),inverse(add(X0,inverse(add(add(X0,X1),inverse(add(inverse(add(add(X0,X1),add(X0,X1))),X2)))))))) = inverse(add(add(X0,X1),add(X0,X1))),
inference(backward_demodulation,[status(thm)],[f795,f97]) ).
fof(f795,plain,
! [X0] : inverse(inverse(add(X0,X0))) = X0,
inference(forward_demodulation,[status(thm)],[f726,f637]) ).
fof(f2921,plain,
! [X0] : inverse(add(add(inverse(add(X0,inverse(add(X0,X0)))),X0),add(inverse(add(X0,inverse(add(X0,X0)))),X0))) = add(inverse(add(inverse(add(X0,inverse(add(X0,X0)))),X0)),inverse(add(X0,X0))),
inference(paramodulation,[status(thm)],[f346,f750]) ).
fof(f2922,plain,
! [X0] : inverse(add(add(inverse(add(X0,inverse(add(X0,X0)))),X0),add(inverse(add(X0,inverse(add(X0,X0)))),X0))) = add(inverse(add(X0,X0)),inverse(add(inverse(add(X0,inverse(add(X0,X0)))),X0))),
inference(paramodulation,[status(thm)],[f346,f750]) ).
fof(f3009,plain,
! [X0] : inverse(add(add(inverse(add(X0,inverse(add(X0,X0)))),X0),add(inverse(add(X0,inverse(add(X0,X0)))),X0))) = inverse(add(X0,X0)),
inference(forward_demodulation,[status(thm)],[f703,f2921]) ).
fof(f3010,plain,
! [X0] : inverse(add(X0,X0)) = add(inverse(add(X0,X0)),inverse(add(inverse(add(X0,inverse(add(X0,X0)))),X0))),
inference(forward_demodulation,[status(thm)],[f3009,f2922]) ).
fof(f3011,plain,
! [X0] : inverse(add(X0,X0)) = add(inverse(add(X0,X0)),inverse(add(X0,X0))),
inference(forward_demodulation,[status(thm)],[f346,f3010]) ).
fof(f3012,plain,
! [X0] : inverse(add(X0,X0)) = inverse(add(add(X0,X0),add(X0,X0))),
inference(forward_demodulation,[status(thm)],[f750,f3011]) ).
fof(f3182,plain,
! [X0] : inverse(add(inverse(X0),inverse(X0))) = inverse(add(inverse(add(X0,X0)),add(inverse(X0),inverse(X0)))),
inference(paramodulation,[status(thm)],[f750,f3012]) ).
fof(f3227,plain,
! [X0] : inverse(inverse(add(X0,X0))) = inverse(add(inverse(add(X0,X0)),add(inverse(X0),inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f750,f3182]) ).
fof(f3228,plain,
! [X0] : X0 = inverse(add(inverse(add(X0,X0)),add(inverse(X0),inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f795,f3227]) ).
fof(f3229,plain,
! [X0] : X0 = inverse(add(inverse(add(X0,X0)),inverse(add(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f750,f3228]) ).
fof(f3230,plain,
! [X0] : X0 = inverse(inverse(add(add(X0,X0),add(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f750,f3229]) ).
fof(f3236,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(backward_demodulation,[status(thm)],[f3293,f795]) ).
fof(f3249,plain,
! [X0,X1,X2] : inverse(add(add(X0,X1),inverse(add(X0,inverse(add(add(X0,X1),inverse(add(inverse(add(add(X0,X1),add(X0,X1))),X2)))))))) = inverse(add(X0,X1)),
inference(backward_demodulation,[status(thm)],[f3293,f794]) ).
fof(f3286,plain,
! [X0,X1] : inverse(X0) = add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))),
inference(backward_demodulation,[status(thm)],[f3293,f737]) ).
fof(f3287,plain,
! [X0,X1] : inverse(X0) = add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))),
inference(backward_demodulation,[status(thm)],[f3293,f726]) ).
fof(f3293,plain,
! [X0] : X0 = add(X0,X0),
inference(forward_demodulation,[status(thm)],[f795,f3230]) ).
fof(f3709,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5)))))))) = inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),
inference(backward_demodulation,[status(thm)],[f3236,f184]) ).
fof(f3724,plain,
! [X0,X1,X2] : inverse(add(X0,inverse(add(inverse(add(X0,X1)),inverse(add(inverse(inverse(add(X0,X1))),X2)))))) = inverse(add(X0,X1)),
inference(backward_demodulation,[status(thm)],[f3236,f259]) ).
fof(f3817,plain,
! [X0,X1,X2,X3] : inverse(add(X0,inverse(add(inverse(X1),inverse(add(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2))))),inverse(add(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2)))))),X3)))))))) = inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2)))))),
inference(backward_demodulation,[status(thm)],[f3236,f525]) ).
fof(f3911,plain,
! [X0,X1,X2] : inverse(add(X0,X1)) = inverse(add(add(X0,X1),inverse(add(inverse(add(X0,X1)),inverse(add(add(X0,X1),X2)))))),
inference(backward_demodulation,[status(thm)],[f3912,f274]) ).
fof(f3912,plain,
! [X0,X1,X2] : inverse(add(add(X0,X1),inverse(add(X0,inverse(add(add(X0,X1),inverse(add(inverse(add(X0,X1)),X2)))))))) = inverse(add(X0,X1)),
inference(forward_demodulation,[status(thm)],[f3293,f3249]) ).
fof(f4306,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5)))))))) = inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),
inference(forward_demodulation,[status(thm)],[f3236,f3709]) ).
fof(f4307,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),add(inverse(X0),inverse(add(X0,X1))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5)))))))) = inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),
inference(forward_demodulation,[status(thm)],[f3236,f4306]) ).
fof(f4308,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),add(inverse(X0),inverse(add(X0,X1))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(add(inverse(X0),inverse(add(X0,X1))),X5)))))))) = inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),
inference(forward_demodulation,[status(thm)],[f3236,f4307]) ).
fof(f4309,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),add(inverse(X0),inverse(add(X0,X1))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(add(inverse(X0),inverse(add(X0,X1))),X5)))))))) = add(inverse(X0),inverse(add(X0,X1))),
inference(forward_demodulation,[status(thm)],[f3236,f4308]) ).
fof(f4362,plain,
! [X0,X1,X2] : inverse(add(X0,inverse(add(inverse(add(X0,X1)),inverse(add(add(X0,X1),X2)))))) = inverse(add(X0,X1)),
inference(forward_demodulation,[status(thm)],[f3236,f3724]) ).
fof(f4770,plain,
! [X0,X1] : inverse(X0) = add(inverse(add(inverse(X1),X0)),inverse(add(X1,X0))),
inference(paramodulation,[status(thm)],[f522,f3236]) ).
fof(f5430,plain,
! [X0,X1,X2] : inverse(add(X0,inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(add(inverse(X0),inverse(add(X0,X1))),X2)))))))) = add(inverse(X0),inverse(add(X0,X1))),
inference(paramodulation,[status(thm)],[f4770,f4309]) ).
fof(f5572,plain,
! [X0,X1,X2] : inverse(add(X0,inverse(add(add(inverse(X0),inverse(add(X0,X1))),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(add(inverse(X0),inverse(add(X0,X1))),X2)))))))) = add(inverse(X0),inverse(add(X0,X1))),
inference(forward_demodulation,[status(thm)],[f3236,f5430]) ).
fof(f5573,plain,
! [X0,X1,X2] : inverse(add(X0,X1)) = add(inverse(add(X0,X1)),inverse(add(add(X0,X1),X2))),
inference(backward_demodulation,[status(thm)],[f5580,f3911]) ).
fof(f5577,plain,
! [X0,X1] : inverse(X0) = add(inverse(X0),add(inverse(X0),inverse(add(X0,X1)))),
inference(backward_demodulation,[status(thm)],[f5580,f3286]) ).
fof(f5580,plain,
! [X0,X1] : inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1)))))) = add(inverse(X0),inverse(add(X0,X1))),
inference(forward_demodulation,[status(thm)],[f3911,f5572]) ).
fof(f6862,plain,
! [X0,X1] : inverse(add(X0,inverse(inverse(add(X0,X1))))) = inverse(add(X0,X1)),
inference(backward_demodulation,[status(thm)],[f5573,f4362]) ).
fof(f6944,plain,
! [X0,X1] : inverse(add(X0,add(X0,X1))) = inverse(add(X0,X1)),
inference(forward_demodulation,[status(thm)],[f3236,f6862]) ).
fof(f6981,plain,
! [X0,X1] : inverse(inverse(add(X0,X1))) = add(X0,add(X0,X1)),
inference(paramodulation,[status(thm)],[f6944,f3236]) ).
fof(f7032,plain,
! [X0,X1] : inverse(X0) = add(inverse(X0),inverse(add(X0,X1))),
inference(backward_demodulation,[status(thm)],[f7043,f5577]) ).
fof(f7043,plain,
! [X0,X1] : add(X0,X1) = add(X0,add(X0,X1)),
inference(forward_demodulation,[status(thm)],[f3236,f6981]) ).
fof(f7135,plain,
! [X0,X1,X2,X3] : inverse(add(X0,inverse(add(inverse(X1),inverse(add(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2))))),inverse(add(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2)))))),X3)))))))) = inverse(add(X1,inverse(inverse(X0)))),
inference(backward_demodulation,[status(thm)],[f7032,f3817]) ).
fof(f7635,plain,
! [X0,X1,X2,X3] : inverse(add(X0,inverse(add(inverse(X1),inverse(add(add(X1,inverse(inverse(X0))),inverse(add(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2)))))),X3)))))))) = inverse(add(X1,inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f7032,f7135]) ).
fof(f7636,plain,
! [X0,X1,X2,X3] : inverse(add(X0,inverse(add(inverse(X1),inverse(add(add(X1,X0),inverse(add(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X2)))))),X3)))))))) = inverse(add(X1,inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f3236,f7635]) ).
fof(f7637,plain,
! [X0,X1,X2] : inverse(add(X0,inverse(add(inverse(X1),inverse(add(add(X1,X0),inverse(add(inverse(add(X1,inverse(inverse(X0)))),X2)))))))) = inverse(add(X1,inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f7032,f7636]) ).
fof(f7638,plain,
! [X0,X1,X2] : inverse(add(X0,inverse(add(inverse(X1),inverse(add(add(X1,X0),inverse(add(inverse(add(X1,X0)),X2)))))))) = inverse(add(X1,inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f3236,f7637]) ).
fof(f7639,plain,
! [X0,X1,X2] : inverse(add(X0,inverse(add(inverse(X1),inverse(add(add(X1,X0),inverse(add(inverse(add(X1,X0)),X2)))))))) = inverse(add(X1,X0)),
inference(forward_demodulation,[status(thm)],[f3236,f7638]) ).
fof(f8410,plain,
! [X0,X1] : inverse(inverse(X0)) = add(X0,inverse(add(inverse(X0),X1))),
inference(paramodulation,[status(thm)],[f3236,f7032]) ).
fof(f8477,plain,
! [X0,X1] : inverse(add(X0,inverse(add(inverse(X1),inverse(add(X1,X0)))))) = inverse(add(X1,X0)),
inference(backward_demodulation,[status(thm)],[f8503,f7639]) ).
fof(f8503,plain,
! [X0,X1] : X0 = add(X0,inverse(add(inverse(X0),X1))),
inference(forward_demodulation,[status(thm)],[f3236,f8410]) ).
fof(f8614,plain,
! [X0,X1] : inverse(add(X0,inverse(inverse(X1)))) = inverse(add(X1,X0)),
inference(forward_demodulation,[status(thm)],[f7032,f8477]) ).
fof(f8615,plain,
! [X0,X1] : inverse(add(X0,X1)) = inverse(add(X1,X0)),
inference(forward_demodulation,[status(thm)],[f3236,f8614]) ).
fof(f8941,plain,
! [X0,X1] : inverse(X0) = add(inverse(add(X1,X0)),inverse(add(X0,inverse(X1)))),
inference(paramodulation,[status(thm)],[f8615,f3287]) ).
fof(f8953,plain,
add(inverse(add(b,inverse(a))),inverse(add(inverse(a),inverse(b)))) != a,
inference(paramodulation,[status(thm)],[f8615,f4]) ).
fof(f8995,plain,
inverse(inverse(a)) != a,
inference(forward_demodulation,[status(thm)],[f8941,f8953]) ).
fof(f8996,plain,
a != a,
inference(forward_demodulation,[status(thm)],[f3236,f8995]) ).
fof(f8997,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f8996]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO074-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.47 % Computer : n017.cluster.edu
% 0.20/0.47 % Model : x86_64 x86_64
% 0.20/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.47 % Memory : 8046.5625MB
% 0.20/0.47 % OS : Linux 6.8.0-71-generic
% 0.20/0.47 % CPULimit : 300
% 0.20/0.47 % WCLimit : 300
% 0.20/0.47 % DateTime : Mon Sep 21 13:47:27 UTC 2026
% 0.20/0.47 % CPUTime :
% 0.20/0.49 % Drodi V4.1.1
% 103.78/13.67 % Refutation found
% 103.78/13.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 103.78/13.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 18.49/13.90 % Elapsed time: 13.400271 seconds
% 18.49/13.90 % CPU time: 105.593583 seconds
% 18.49/13.90 % Total memory used: 1.683 GB
% 18.49/13.90 % Net memory used: 1.666 GB
%------------------------------------------------------------------------------