%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO072-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:50 PM UTC 2026
% Result : Unsatisfiable 38.02s 5.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO072-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n014.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 13:51:49 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 38.02/5.25 % Refutation found
% 38.02/5.25 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 38.02/5.25 % SZS output start CNFRefutation for theBenchmark
% 38.02/5.25 fof(f1,axiom,(
% 38.02/5.25 (![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 ))),
% 38.02/5.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.02/5.25 fof(f2,negated_conjecture,(
% 38.02/5.25 add(b,a) != add(a,b) ),
% 38.02/5.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 38.02/5.25 fof(f3,plain,(
% 38.02/5.25 ![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)),
% 38.02/5.25 inference(cnf_transformation,[status(thm)],[f1])).
% 38.02/5.25 fof(f4,plain,(
% 38.02/5.25 ~add(b,a)=add(a,b)),
% 38.02/5.25 inference(cnf_transformation,[status(thm)],[f2])).
% 38.02/5.25 fof(f8,plain,(
% 38.02/5.25 ![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)))))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f3,f3])).
% 38.02/5.25 fof(f10,plain,(
% 38.02/5.25 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(X0)),X1)),X0)),X2)),inverse(X0))),X0))=inverse(X0))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f3,f3])).
% 38.02/5.25 fof(f13,plain,(
% 38.02/5.25 ![X0]: (inverse(add(inverse(add(X0,inverse(X0))),X0))=inverse(X0))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f3,f10])).
% 38.02/5.25 fof(f34,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))))=X0)),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f13,f3])).
% 38.02/5.25 fof(f52,plain,(
% 38.02/5.25 ![X0]: (inverse(add(inverse(X0),inverse(add(X0,X0))))=X0)),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f34,f34])).
% 38.02/5.25 fof(f64,plain,(
% 38.02/5.25 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(X0,X1)),X2)),inverse(add(X0,X2))))=X2)),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f34,f3])).
% 38.02/5.25 fof(f92,plain,(
% 38.02/5.25 ![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))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f52,f3])).
% 38.02/5.25 fof(f117,plain,(
% 38.02/5.25 ![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)))))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f34,f8])).
% 38.02/5.25 fof(f120,plain,(
% 38.02/5.25 ![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)))))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f10,f8])).
% 38.02/5.25 fof(f165,plain,(
% 38.02/5.25 ![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)))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f8,f34])).
% 38.02/5.25 fof(f178,plain,(
% 38.02/5.25 ![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)))))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f10,f120])).
% 38.02/5.25 fof(f179,plain,(
% 38.02/5.25 ![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))))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f10,f178])).
% 38.02/5.25 fof(f254,plain,(
% 38.02/5.25 ![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)))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f117,f165])).
% 38.02/5.25 fof(f269,plain,(
% 38.02/5.25 ![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)))))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f34,f64])).
% 38.02/5.25 fof(f276,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(inverse(add(X0,X1)),inverse(add(inverse(X0),X1))))=X1)),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f34,f64])).
% 38.02/5.25 fof(f338,plain,(
% 38.02/5.25 ![X0]: (inverse(add(inverse(add(add(X0,inverse(X0)),X0)),inverse(X0)))=X0)),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f13,f276])).
% 38.02/5.25 fof(f341,plain,(
% 38.02/5.25 ![X0]: (inverse(add(inverse(add(X0,inverse(add(X0,X0)))),X0))=inverse(add(X0,X0)))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f52,f276])).
% 38.02/5.25 fof(f353,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(X0,inverse(add(X1,inverse(add(inverse(X1),X0))))))=inverse(add(inverse(X1),X0)))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f276,f64])).
% 38.02/5.25 fof(f427,plain,(
% 38.02/5.25 ![X0]: (inverse(add(X0,inverse(add(add(X0,inverse(X0)),inverse(X0)))))=inverse(X0))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f338,f64])).
% 38.02/5.25 fof(f517,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(inverse(add(inverse(X0),X1)),inverse(add(X0,X1))))=X1)),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f427,f64])).
% 38.02/5.25 fof(f520,plain,(
% 38.02/5.25 ![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)))))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f427,f8])).
% 38.02/5.25 fof(f521,plain,(
% 38.02/5.25 ![X0]: (inverse(add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(X0)))))))=X0)),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f427,f34])).
% 38.02/5.25 fof(f582,plain,(
% 38.02/5.25 ![X0]: (inverse(add(inverse(X0),inverse(X0)))=X0)),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f353,f521])).
% 38.02/5.25 fof(f602,plain,(
% 38.02/5.25 ![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))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f64,f582])).
% 38.02/5.25 fof(f604,plain,(
% 38.02/5.25 ![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))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f276,f582])).
% 38.02/5.25 fof(f605,plain,(
% 38.02/5.25 ![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))))))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f34,f582])).
% 38.02/5.25 fof(f607,plain,(
% 38.02/5.25 ![X0]: (inverse(add(X0,inverse(add(inverse(X0),inverse(X0)))))=add(inverse(X0),inverse(X0)))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f582,f582])).
% 38.02/5.25 fof(f632,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(inverse(add(X0,X1)),inverse(add(inverse(X0),X1))))=X1)),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f582,f64])).
% 38.02/5.25 fof(f698,plain,(
% 38.02/5.25 ![X0,X1,X2]: (inverse(add(X0,X0))=add(inverse(add(inverse(add(X1,X2)),X0)),inverse(add(X1,X0))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f64,f602])).
% 38.02/5.25 fof(f721,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(X0,X0))=add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f276,f604])).
% 38.02/5.25 fof(f732,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(X0,X0))=add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f34,f605])).
% 38.02/5.25 fof(f745,plain,(
% 38.02/5.25 ![X0]: (inverse(add(X0,X0))=add(inverse(X0),inverse(X0)))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f582,f607])).
% 38.02/5.25 fof(f789,plain,(
% 38.02/5.25 ![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))))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f790,f92])).
% 38.02/5.25 fof(f790,plain,(
% 38.02/5.25 ![X0]: (inverse(inverse(add(X0,X0)))=X0)),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f721,f632])).
% 38.02/5.25 fof(f2916,plain,(
% 38.02/5.25 ![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))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f341,f745])).
% 38.02/5.25 fof(f2917,plain,(
% 38.02/5.25 ![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))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f341,f745])).
% 38.02/5.25 fof(f3004,plain,(
% 38.02/5.25 ![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)))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f698,f2916])).
% 38.02/5.25 fof(f3005,plain,(
% 38.02/5.25 ![X0]: (inverse(add(X0,X0))=add(inverse(add(X0,X0)),inverse(add(inverse(add(X0,inverse(add(X0,X0)))),X0))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3004,f2917])).
% 38.02/5.25 fof(f3006,plain,(
% 38.02/5.25 ![X0]: (inverse(add(X0,X0))=add(inverse(add(X0,X0)),inverse(add(X0,X0))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f341,f3005])).
% 38.02/5.25 fof(f3007,plain,(
% 38.02/5.25 ![X0]: (inverse(add(X0,X0))=inverse(add(add(X0,X0),add(X0,X0))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f745,f3006])).
% 38.02/5.25 fof(f3177,plain,(
% 38.02/5.25 ![X0]: (inverse(add(inverse(X0),inverse(X0)))=inverse(add(inverse(add(X0,X0)),add(inverse(X0),inverse(X0)))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f745,f3007])).
% 38.02/5.25 fof(f3222,plain,(
% 38.02/5.25 ![X0]: (inverse(inverse(add(X0,X0)))=inverse(add(inverse(add(X0,X0)),add(inverse(X0),inverse(X0)))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f745,f3177])).
% 38.02/5.25 fof(f3223,plain,(
% 38.02/5.25 ![X0]: (X0=inverse(add(inverse(add(X0,X0)),add(inverse(X0),inverse(X0)))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f790,f3222])).
% 38.02/5.25 fof(f3224,plain,(
% 38.02/5.25 ![X0]: (X0=inverse(add(inverse(add(X0,X0)),inverse(add(X0,X0)))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f745,f3223])).
% 38.02/5.25 fof(f3225,plain,(
% 38.02/5.25 ![X0]: (X0=inverse(inverse(add(add(X0,X0),add(X0,X0)))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f745,f3224])).
% 38.02/5.25 fof(f3231,plain,(
% 38.02/5.25 ![X0]: (inverse(inverse(X0))=X0)),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f3288,f790])).
% 38.02/5.25 fof(f3244,plain,(
% 38.02/5.25 ![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)))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f3288,f789])).
% 38.02/5.25 fof(f3281,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(X0)=add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f3288,f732])).
% 38.02/5.25 fof(f3288,plain,(
% 38.02/5.25 ![X0]: (X0=add(X0,X0))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f790,f3225])).
% 38.02/5.25 fof(f3704,plain,(
% 38.02/5.25 ![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))))))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f3231,f179])).
% 38.02/5.25 fof(f3719,plain,(
% 38.02/5.25 ![X0,X1,X2]: (inverse(add(X0,inverse(add(inverse(add(X0,X1)),inverse(add(inverse(inverse(add(X0,X1))),X2))))))=inverse(add(X0,X1)))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f3231,f254])).
% 38.02/5.25 fof(f3812,plain,(
% 38.02/5.25 ![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)))))))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f3231,f520])).
% 38.02/5.25 fof(f3906,plain,(
% 38.02/5.25 ![X0,X1,X2]: (inverse(add(X0,X1))=inverse(add(add(X0,X1),inverse(add(inverse(add(X0,X1)),inverse(add(add(X0,X1),X2)))))))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f3907,f269])).
% 38.02/5.25 fof(f3907,plain,(
% 38.02/5.25 ![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)))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3288,f3244])).
% 38.02/5.25 fof(f4301,plain,(
% 38.02/5.25 ![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))))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f3704])).
% 38.02/5.25 fof(f4302,plain,(
% 38.02/5.25 ![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))))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f4301])).
% 38.02/5.25 fof(f4303,plain,(
% 38.02/5.25 ![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))))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f4302])).
% 38.02/5.25 fof(f4304,plain,(
% 38.02/5.25 ![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))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f4303])).
% 38.02/5.25 fof(f4357,plain,(
% 38.02/5.25 ![X0,X1,X2]: (inverse(add(X0,inverse(add(inverse(add(X0,X1)),inverse(add(add(X0,X1),X2))))))=inverse(add(X0,X1)))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f3719])).
% 38.02/5.25 fof(f4765,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(X0)=add(inverse(add(inverse(X1),X0)),inverse(add(X1,X0))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f517,f3231])).
% 38.02/5.25 fof(f5425,plain,(
% 38.02/5.25 ![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))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f4765,f4304])).
% 38.02/5.25 fof(f5567,plain,(
% 38.02/5.25 ![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))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f5425])).
% 38.02/5.25 fof(f5568,plain,(
% 38.02/5.25 ![X0,X1,X2]: (inverse(add(X0,X1))=add(inverse(add(X0,X1)),inverse(add(add(X0,X1),X2))))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f5575,f3906])).
% 38.02/5.25 fof(f5572,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(X0)=add(inverse(X0),add(inverse(X0),inverse(add(X0,X1)))))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f5575,f3281])).
% 38.02/5.25 fof(f5575,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))=add(inverse(X0),inverse(add(X0,X1))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3906,f5567])).
% 38.02/5.25 fof(f6857,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(X0,inverse(inverse(add(X0,X1)))))=inverse(add(X0,X1)))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f5568,f4357])).
% 38.02/5.25 fof(f6939,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(X0,add(X0,X1)))=inverse(add(X0,X1)))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f6857])).
% 38.02/5.25 fof(f6976,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(inverse(add(X0,X1)))=add(X0,add(X0,X1)))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f6939,f3231])).
% 38.02/5.25 fof(f7027,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(X0)=add(inverse(X0),inverse(add(X0,X1))))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f7038,f5572])).
% 38.02/5.25 fof(f7038,plain,(
% 38.02/5.25 ![X0,X1]: (add(X0,X1)=add(X0,add(X0,X1)))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f6976])).
% 38.02/5.25 fof(f7130,plain,(
% 38.02/5.25 ![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)))))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f7027,f3812])).
% 38.02/5.25 fof(f7630,plain,(
% 38.02/5.25 ![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)))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f7027,f7130])).
% 38.02/5.25 fof(f7631,plain,(
% 38.02/5.25 ![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)))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f7630])).
% 38.02/5.25 fof(f7632,plain,(
% 38.02/5.25 ![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)))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f7027,f7631])).
% 38.02/5.25 fof(f7633,plain,(
% 38.02/5.25 ![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)))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f7632])).
% 38.02/5.25 fof(f7634,plain,(
% 38.02/5.25 ![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)))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f7633])).
% 38.02/5.25 fof(f8405,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(inverse(X0))=add(X0,inverse(add(inverse(X0),X1))))),
% 38.02/5.25 inference(paramodulation,[status(thm)],[f3231,f7027])).
% 38.02/5.25 fof(f8472,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(X0,inverse(add(inverse(X1),inverse(add(X1,X0))))))=inverse(add(X1,X0)))),
% 38.02/5.25 inference(backward_demodulation,[status(thm)],[f8498,f7634])).
% 38.02/5.25 fof(f8498,plain,(
% 38.02/5.25 ![X0,X1]: (X0=add(X0,inverse(add(inverse(X0),X1))))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f3231,f8405])).
% 38.02/5.25 fof(f8609,plain,(
% 38.02/5.25 ![X0,X1]: (inverse(add(X0,inverse(inverse(X1))))=inverse(add(X1,X0)))),
% 38.02/5.25 inference(forward_demodulation,[status(thm)],[f7027,f8472])).
% 38.02/5.29 fof(f8610,plain,(
% 38.02/5.29 ![X0,X1]: (inverse(add(X0,X1))=inverse(add(X1,X0)))),
% 38.02/5.29 inference(forward_demodulation,[status(thm)],[f3231,f8609])).
% 38.02/5.29 fof(f8945,plain,(
% 38.02/5.29 ![X0,X1]: (inverse(inverse(add(X0,X1)))=add(X1,X0))),
% 38.02/5.29 inference(paramodulation,[status(thm)],[f8610,f3231])).
% 38.02/5.29 fof(f8987,plain,(
% 38.02/5.29 ![X0,X1]: (add(X0,X1)=add(X1,X0))),
% 38.02/5.29 inference(forward_demodulation,[status(thm)],[f3231,f8945])).
% 38.02/5.29 fof(f8988,plain,(
% 38.02/5.29 $false),
% 38.02/5.29 inference(backward_subsumption_resolution,[status(thm)],[f4,f8987])).
% 38.02/5.29 % SZS output end CNFRefutation for theBenchmark.p
% 16.39/5.50 % Elapsed time: 5.114732 seconds
% 16.39/5.50 % CPU time: 39.821844 seconds
% 16.39/5.50 % Total memory used: 1.411 GB
% 16.39/5.50 % Net memory used: 1.380 GB
%------------------------------------------------------------------------------