%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP419-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n001.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 : Fri Sep 25 01:26:28 PM UTC 2026
% Result : Unsatisfiable 35.49s 5.33s
% Output : CNFRefutation 35.49s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t7,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,axiom,
sF1 = multiply(inverse(b2),b2),
introduced(definition) ).
cnf(t1,axiom,
sF0 = inverse(b2),
introduced(definition) ).
cnf(t4,plain,
inverse(b2) = sF0,
inference(orient,[status(thm)],[t1]) ).
cnf(t7981,plain,
sF1 = multiply(sF0,b2),
inference(step,[status(thm)],[t2,t4]) ).
cnf(t5,plain,
multiply(sF0,b2) = sF1,
inference(orient,[status(thm)],[t7981]) ).
cnf(t10,plain,
X1 = inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),sF1)),
inference(cp,[status(thm)],[t7,t5]) ).
cnf(t7984,plain,
X1 = inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(multiply(sF0,b2)))))))),sF1)),
inference(step,[status(thm)],[t10,t4]) ).
cnf(t7985,plain,
X1 = inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(step,[status(thm)],[t7984,t5]) ).
cnf(t14,plain,
inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1)) = X1,
inference(orient,[status(thm)],[t7985]) ).
cnf(t17,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(cp,[status(thm)],[t14,t14]) ).
cnf(t24,plain,
inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t17]) ).
cnf(t12,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4))),
inference(cp,[status(thm)],[t7,t7]) ).
cnf(t92,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = inverse(multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4))),
inference(orient,[status(thm)],[t12]) ).
cnf(t98,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3))) = multiply(inverse(multiply(Y3,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4)),
inference(cp,[status(thm)],[t92,t24]) ).
cnf(t8030,plain,
multiply(inverse(multiply(f1,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)) = multiply(inverse(multiply(Y3,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4)),
inference(step,[status(thm)],[t98,t92]) ).
cnf(t96,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3))) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(multiply(sF0,b2)))))))),multiply(Y3,b2)),
inference(cp,[status(thm)],[t92,t4]) ).
cnf(t8002,plain,
multiply(inverse(multiply(f1,inverse(multiply(inverse(X2),inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(multiply(sF0,b2)))))))),multiply(Y3,b2)),
inference(step,[status(thm)],[t96,t92]) ).
cnf(t8003,plain,
multiply(inverse(multiply(f1,inverse(multiply(inverse(X2),inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),multiply(Y3,b2)),
inference(step,[status(thm)],[t8002,t5]) ).
cnf(t7986,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1))))))),sF1) = X1,
inference(step,[status(thm)],[t14,t24]) ).
cnf(t25,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1))))))),sF1) = X1,
inference(rw,[status(thm)],[t7986]) ).
cnf(t31,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1))))))),sF1) = X1,
inference(orient,[status(thm)],[t25]) ).
cnf(t9,plain,
X1 = inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(multiply(sF0,b2)))))))),multiply(X2,b2))),
inference(cp,[status(thm)],[t7,t4]) ).
cnf(t7988,plain,
X1 = inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),multiply(X2,b2))),
inference(step,[status(thm)],[t9,t5]) ).
cnf(t34,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),multiply(X1,b2))) = X2,
inference(orient,[status(thm)],[t7988]) ).
cnf(t41,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),multiply(X1,b2)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(cp,[status(thm)],[t31,t34]) ).
cnf(t64,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),multiply(X1,b2)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t41]) ).
cnf(t66,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3))),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),multiply(Y3,b2)),
inference(cp,[status(thm)],[t64,t7]) ).
cnf(t7990,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(Y3,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),multiply(Y3,b2)),
inference(step,[status(thm)],[t66,t7]) ).
cnf(t69,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),multiply(X1,b2)) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t7990]) ).
cnf(t8004,plain,
multiply(inverse(multiply(f1,inverse(multiply(inverse(X2),inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(step,[status(thm)],[t8003,t69]) ).
cnf(t127,plain,
multiply(inverse(multiply(f1,inverse(multiply(inverse(X1),inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8004]) ).
cnf(t130,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(f1,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)),
inference(cp,[status(thm)],[t127,t24]) ).
cnf(t8006,plain,
multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(f1,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)),
inference(step,[status(thm)],[t130,t24]) ).
cnf(t135,plain,
multiply(inverse(multiply(f1,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)) = multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8006]) ).
cnf(t139,plain,
multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(f1,inverse(multiply(X1,inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)),
inference(cp,[status(thm)],[t135,t31]) ).
cnf(t8008,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(f1,inverse(multiply(X1,inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)),
inference(step,[status(thm)],[t139,t31]) ).
cnf(t143,plain,
multiply(inverse(multiply(f1,inverse(multiply(X1,inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8008]) ).
cnf(t8031,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(Y3,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4)),
inference(step,[status(thm)],[t8030,t143]) ).
cnf(t8032,plain,
multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(Y3,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(Y4,inverse(multiply(inverse(Y4),Y4)))))))),multiply(Y3,Y4)),
inference(step,[status(thm)],[t8031,t24]) ).
cnf(t198,plain,
multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8032]) ).
cnf(t204,plain,
multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X2,X3)),
inference(cp,[status(thm)],[t198,t31]) ).
cnf(t8047,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X2,X3)),
inference(step,[status(thm)],[t204,t31]) ).
cnf(t273,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8047]) ).
cnf(t281,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X2)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X2),
inference(cp,[status(thm)],[t273,t31]) ).
cnf(t315,plain,
multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X2,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X1) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t281]) ).
cnf(t318,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))))),inverse(multiply(b2,inverse(sF1))))))),sF1) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)))),sF1)),
inference(cp,[status(thm)],[t24,t315]) ).
cnf(t8263,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)))),sF1)),
inference(step,[status(thm)],[t318,t31]) ).
cnf(t8264,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1)),
inference(step,[status(thm)],[t8263,t24]) ).
cnf(t320,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X2,b2)),
inference(cp,[status(thm)],[t69,t315]) ).
cnf(t8052,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X2,b2)),
inference(step,[status(thm)],[t320,t315]) ).
cnf(t8053,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X2,b2)),
inference(step,[status(thm)],[t8052,t24]) ).
cnf(t8054,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1) = multiply(inverse(multiply(X2,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1))),multiply(X2,b2)),
inference(step,[status(thm)],[t8053,t24]) ).
cnf(t330,plain,
multiply(inverse(multiply(X1,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1))),multiply(X1,b2)) = multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1),
inference(orient,[status(thm)],[t8054]) ).
cnf(t333,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1) = multiply(inverse(multiply(X2,X1)),multiply(X2,b2)),
inference(cp,[status(thm)],[t330,t31]) ).
cnf(t8055,plain,
multiply(inverse(multiply(sF0,X1)),sF1) = multiply(inverse(multiply(X2,X1)),multiply(X2,b2)),
inference(step,[status(thm)],[t333,t31]) ).
cnf(t337,plain,
multiply(inverse(multiply(X1,X2)),multiply(X1,b2)) = multiply(inverse(multiply(sF0,X2)),sF1),
inference(orient,[status(thm)],[t8055]) ).
cnf(t356,plain,
multiply(inverse(multiply(sF0,multiply(X1,b2))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,X2)),sF1)),multiply(inverse(multiply(X1,X2)),b2)),
inference(cp,[status(thm)],[t337,t337]) ).
cnf(t376,plain,
multiply(inverse(multiply(inverse(multiply(sF0,X1)),sF1)),multiply(inverse(multiply(X2,X1)),b2)) = multiply(inverse(multiply(sF0,multiply(X2,b2))),sF1),
inference(orient,[status(thm)],[t356]) ).
cnf(t15,plain,
b2 = inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(cp,[status(thm)],[t14,t4]) ).
cnf(t20,plain,
inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)) = b2,
inference(orient,[status(thm)],[t15]) ).
cnf(t7987,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),sF1) = b2,
inference(step,[status(thm)],[t20,t24]) ).
cnf(t26,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),sF1) = b2,
inference(rw,[status(thm)],[t7987]) ).
cnf(t29,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),sF1) = b2,
inference(orient,[status(thm)],[t26]) ).
cnf(t280,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),b2),
inference(cp,[status(thm)],[t273,t29]) ).
cnf(t308,plain,
multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),b2) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t280]) ).
cnf(t393,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),b2))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,b2)),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)),b2)),
inference(cp,[status(thm)],[t376,t308]) ).
cnf(t8069,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,b2)),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)),b2)),
inference(step,[status(thm)],[t393,t308]) ).
cnf(t8070,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1) = multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)),b2)),
inference(step,[status(thm)],[t8069,t5]) ).
cnf(t8071,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1) = multiply(inverse(multiply(inverse(sF1),sF1)),multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),b2)),
inference(step,[status(thm)],[t8070,t24]) ).
cnf(t577,plain,
multiply(inverse(multiply(inverse(sF1),sF1)),multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),b2)) = multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1),
inference(orient,[status(thm)],[t8071]) ).
cnf(t580,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1) = multiply(inverse(multiply(inverse(sF1),sF1)),multiply(X1,b2)),
inference(cp,[status(thm)],[t577,t31]) ).
cnf(t587,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1) = multiply(inverse(multiply(inverse(sF1),sF1)),multiply(X1,b2)),
inference(orient,[status(thm)],[t580]) ).
cnf(t8265,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(inverse(sF1),sF1)),multiply(X1,b2))),
inference(step,[status(thm)],[t8264,t587]) ).
cnf(t5074,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(inverse(sF1),sF1)),multiply(X1,b2))),
inference(orient,[status(thm)],[t8265]) ).
cnf(t5077,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(inverse(multiply(inverse(multiply(inverse(sF1),sF1)),multiply(X1,b2)))),multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(cp,[status(thm)],[t273,t5074]) ).
cnf(t8266,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(inverse(multiply(inverse(multiply(inverse(sF1),sF1)),multiply(X1,b2)))),inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t5077,t31]) ).
cnf(t5086,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(sF1),sF1)),multiply(X1,b2)))),inverse(multiply(b2,inverse(sF1)))) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8266]) ).
cnf(t590,plain,
multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(X1),b2)) = multiply(inverse(multiply(sF0,X1)),sF1),
inference(cp,[status(thm)],[t587,t31]) ).
cnf(t604,plain,
multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(X1),b2)) = multiply(inverse(multiply(sF0,X1)),sF1),
inference(orient,[status(thm)],[t590]) ).
cnf(t5091,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(cp,[status(thm)],[t5086,t604]) ).
cnf(t5136,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(orient,[status(thm)],[t5091]) ).
cnf(t8267,plain,
inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t24,t5136]) ).
cnf(t5137,plain,
inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(orient,[status(thm)],[t8267]) ).
cnf(t5154,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(X1))),sF1))),inverse(multiply(b2,inverse(sF1)))) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1))))),
inference(cp,[status(thm)],[t5137,t5136]) ).
cnf(t8270,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(X1))),sF1))),inverse(multiply(b2,inverse(sF1)))) = X1,
inference(step,[status(thm)],[t31,t5136]) ).
cnf(t5140,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(X1))),sF1))),inverse(multiply(b2,inverse(sF1)))) = X1,
inference(rw,[status(thm)],[t8270]) ).
cnf(t5212,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(X1))),sF1))),inverse(multiply(b2,inverse(sF1)))) = X1,
inference(orient,[status(thm)],[t5140]) ).
cnf(t8402,plain,
X1 = inverse(multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1))))),
inference(step,[status(thm)],[t5154,t5212]) ).
cnf(t5714,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1))))) = X1,
inference(orient,[status(thm)],[t8402]) ).
cnf(t95,plain,
inverse(multiply(inverse(multiply(X1,inverse(multiply(b2,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2))) = multiply(inverse(multiply(X3,inverse(multiply(sF0,inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),multiply(X3,Y3)),
inference(cp,[status(thm)],[t92,t4]) ).
cnf(t8013,plain,
multiply(inverse(multiply(f1,inverse(multiply(inverse(b2),inverse(multiply(f1,inverse(multiply(inverse(f1),f1)))))))),multiply(f1,f1)) = multiply(inverse(multiply(X3,inverse(multiply(sF0,inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),multiply(X3,Y3)),
inference(step,[status(thm)],[t95,t92]) ).
cnf(t8014,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(b2),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X3,inverse(multiply(sF0,inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),multiply(X3,Y3)),
inference(step,[status(thm)],[t8013,t143]) ).
cnf(t8015,plain,
multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X3,inverse(multiply(sF0,inverse(multiply(Y3,inverse(multiply(inverse(Y3),Y3)))))))),multiply(X3,Y3)),
inference(step,[status(thm)],[t8014,t4]) ).
cnf(t150,plain,
multiply(inverse(multiply(X1,inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)) = multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8015]) ).
cnf(t153,plain,
multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X1),
inference(cp,[status(thm)],[t150,t31]) ).
cnf(t163,plain,
multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X1) = multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t153]) ).
cnf(t166,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,b2)),
inference(cp,[status(thm)],[t69,t163]) ).
cnf(t8016,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),sF1) = multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,b2)),
inference(step,[status(thm)],[t166,t163]) ).
cnf(t8017,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1) = multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,b2)),
inference(step,[status(thm)],[t8016,t24]) ).
cnf(t8018,plain,
multiply(inverse(multiply(sF0,b2)),sF1) = multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,b2)),
inference(step,[status(thm)],[t8017,t29]) ).
cnf(t8019,plain,
multiply(inverse(sF1),sF1) = multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,b2)),
inference(step,[status(thm)],[t8018,t5]) ).
cnf(t8020,plain,
multiply(inverse(sF1),sF1) = multiply(inverse(multiply(X1,multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),sF1))),multiply(X1,b2)),
inference(step,[status(thm)],[t8019,t24]) ).
cnf(t8021,plain,
multiply(inverse(sF1),sF1) = multiply(inverse(multiply(X1,b2)),multiply(X1,b2)),
inference(step,[status(thm)],[t8020,t29]) ).
cnf(t174,plain,
multiply(inverse(multiply(X1,b2)),multiply(X1,b2)) = multiply(inverse(sF1),sF1),
inference(orient,[status(thm)],[t8021]) ).
cnf(t288,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(multiply(X3,b2),inverse(multiply(inverse(sF1),sF1)))))))),multiply(X2,multiply(X3,b2))),
inference(cp,[status(thm)],[t273,t174]) ).
cnf(t298,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(X3,b2),inverse(multiply(inverse(sF1),sF1)))))))),multiply(X1,multiply(X3,b2))) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t288]) ).
cnf(t313,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(X3,inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(inverse(sF1),sF1)))))))),multiply(X2,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X3,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),b2))),
inference(cp,[status(thm)],[t298,t308]) ).
cnf(t8224,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(X3,inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(inverse(sF1),sF1)))))))),multiply(X2,multiply(inverse(multiply(sF0,inverse(multiply(X3,inverse(multiply(b2,inverse(sF1))))))),sF1))),
inference(step,[status(thm)],[t313,t308]) ).
cnf(t4142,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(X3,inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(inverse(sF1),sF1)))))))),multiply(X1,multiply(inverse(multiply(sF0,inverse(multiply(X3,inverse(multiply(b2,inverse(sF1))))))),sF1))) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8224]) ).
cnf(t4143,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(b2,inverse(multiply(inverse(sF1),sF1)))))))),multiply(X2,multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),sF1))),
inference(cp,[status(thm)],[t4142,t29]) ).
cnf(t8225,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(b2,inverse(multiply(inverse(sF1),sF1)))))))),multiply(X2,b2)),
inference(step,[status(thm)],[t4143,t29]) ).
cnf(t8226,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(multiply(inverse(sF1),sF1)))))))),sF1),
inference(step,[status(thm)],[t8225,t337]) ).
cnf(t4179,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(multiply(inverse(sF1),sF1)))))))),sF1) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8226]) ).
cnf(t5216,plain,
multiply(X1,inverse(multiply(b2,inverse(multiply(inverse(sF1),sF1))))) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(cp,[status(thm)],[t5212,t4179]) ).
cnf(t8283,plain,
multiply(X1,inverse(multiply(b2,inverse(multiply(inverse(sF1),sF1))))) = multiply(X1,inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t5216,t5212]) ).
cnf(t5228,plain,
multiply(X1,inverse(multiply(b2,inverse(multiply(inverse(sF1),sF1))))) = multiply(X1,inverse(multiply(b2,inverse(sF1)))),
inference(orient,[status(thm)],[t8283]) ).
cnf(t5305,plain,
multiply(b2,inverse(multiply(inverse(sF1),sF1))) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(cp,[status(thm)],[t5212,t5228]) ).
cnf(t8289,plain,
multiply(b2,inverse(multiply(inverse(sF1),sF1))) = multiply(b2,inverse(sF1)),
inference(step,[status(thm)],[t5305,t5212]) ).
cnf(t5306,plain,
multiply(b2,inverse(multiply(inverse(sF1),sF1))) = multiply(b2,inverse(sF1)),
inference(orient,[status(thm)],[t8289]) ).
cnf(t5309,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF1),sF1)))),sF1) = multiply(inverse(multiply(b2,inverse(sF1))),multiply(b2,b2)),
inference(cp,[status(thm)],[t337,t5306]) ).
cnf(t8291,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF1),sF1)))),sF1) = multiply(inverse(multiply(sF0,inverse(sF1))),sF1),
inference(step,[status(thm)],[t5309,t337]) ).
cnf(t5314,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF1),sF1)))),sF1) = multiply(inverse(multiply(sF0,inverse(sF1))),sF1),
inference(orient,[status(thm)],[t8291]) ).
cnf(t5330,plain,
multiply(inverse(sF1),sF1) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(sF1))),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(cp,[status(thm)],[t5212,t5314]) ).
cnf(t8294,plain,
multiply(inverse(sF1),sF1) = sF1,
inference(step,[status(thm)],[t5330,t5212]) ).
cnf(t5354,plain,
multiply(inverse(sF1),sF1) = sF1,
inference(orient,[status(thm)],[t8294]) ).
cnf(t8303,plain,
multiply(inverse(sF1),multiply(inverse(X1),b2)) = multiply(inverse(multiply(sF0,X1)),sF1),
inference(step,[status(thm)],[t604,t5354]) ).
cnf(t5367,plain,
multiply(inverse(sF1),multiply(inverse(X1),b2)) = multiply(inverse(multiply(sF0,X1)),sF1),
inference(rw,[status(thm)],[t8303]) ).
cnf(t5449,plain,
multiply(inverse(sF1),multiply(inverse(X1),b2)) = multiply(inverse(multiply(sF0,X1)),sF1),
inference(orient,[status(thm)],[t5367]) ).
cnf(t608,plain,
multiply(inverse(multiply(sF0,multiply(inverse(X1),b2))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,X1)),sF1)),multiply(inverse(multiply(inverse(sF1),sF1)),b2)),
inference(cp,[status(thm)],[t337,t604]) ).
cnf(t648,plain,
multiply(inverse(multiply(inverse(multiply(sF0,X1)),sF1)),multiply(inverse(multiply(inverse(sF1),sF1)),b2)) = multiply(inverse(multiply(sF0,multiply(inverse(X1),b2))),sF1),
inference(orient,[status(thm)],[t608]) ).
cnf(t661,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(inverse(sF1),sF1)),b2))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,multiply(inverse(X1),b2))),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,X1)),sF1)),b2)),
inference(cp,[status(thm)],[t337,t648]) ).
cnf(t589,plain,
multiply(inverse(multiply(inverse(sF1),sF1)),multiply(sF0,b2)) = multiply(inverse(multiply(sF0,b2)),sF1),
inference(cp,[status(thm)],[t587,t29]) ).
cnf(t8072,plain,
multiply(inverse(multiply(inverse(sF1),sF1)),sF1) = multiply(inverse(multiply(sF0,b2)),sF1),
inference(step,[status(thm)],[t589,t5]) ).
cnf(t8073,plain,
multiply(inverse(multiply(inverse(sF1),sF1)),sF1) = multiply(inverse(sF1),sF1),
inference(step,[status(thm)],[t8072,t5]) ).
cnf(t599,plain,
multiply(inverse(multiply(inverse(sF1),sF1)),sF1) = multiply(inverse(sF1),sF1),
inference(orient,[status(thm)],[t8073]) ).
cnf(t602,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(inverse(sF1),sF1)),b2))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,sF1)),sF1)),multiply(inverse(multiply(inverse(sF1),sF1)),b2)),
inference(cp,[status(thm)],[t376,t599]) ).
cnf(t8075,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(inverse(sF1),sF1)),b2))),sF1) = multiply(inverse(multiply(sF0,multiply(inverse(sF1),b2))),sF1),
inference(step,[status(thm)],[t602,t376]) ).
cnf(t611,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(inverse(sF1),sF1)),b2))),sF1) = multiply(inverse(multiply(sF0,multiply(inverse(sF1),b2))),sF1),
inference(orient,[status(thm)],[t8075]) ).
cnf(t8081,plain,
multiply(inverse(multiply(sF0,multiply(inverse(sF1),b2))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,multiply(inverse(X1),b2))),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,X1)),sF1)),b2)),
inference(step,[status(thm)],[t661,t611]) ).
cnf(t395,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(X1,X2)),b2))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,multiply(X1,b2))),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,X2)),sF1)),b2)),
inference(cp,[status(thm)],[t376,t337]) ).
cnf(t520,plain,
multiply(inverse(multiply(inverse(multiply(sF0,multiply(X1,b2))),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,X2)),sF1)),b2)) = multiply(inverse(multiply(sF0,multiply(inverse(multiply(X1,X2)),b2))),sF1),
inference(orient,[status(thm)],[t395]) ).
cnf(t8082,plain,
multiply(inverse(multiply(sF0,multiply(inverse(sF1),b2))),sF1) = multiply(inverse(multiply(sF0,multiply(inverse(multiply(inverse(X1),X1)),b2))),sF1),
inference(step,[status(thm)],[t8081,t520]) ).
cnf(t663,plain,
multiply(inverse(multiply(sF0,multiply(inverse(multiply(inverse(X1),X1)),b2))),sF1) = multiply(inverse(multiply(sF0,multiply(inverse(sF1),b2))),sF1),
inference(orient,[status(thm)],[t8082]) ).
cnf(t5720,plain,
multiply(inverse(multiply(inverse(X1),X1)),b2) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(sF0,multiply(inverse(sF1),b2))),sF1))),inverse(multiply(b2,inverse(sF1))))),
inference(cp,[status(thm)],[t5714,t663]) ).
cnf(t8403,plain,
multiply(inverse(multiply(inverse(X1),X1)),b2) = multiply(inverse(sF1),b2),
inference(step,[status(thm)],[t5720,t5714]) ).
cnf(t5864,plain,
multiply(inverse(multiply(inverse(X1),X1)),b2) = multiply(inverse(sF1),b2),
inference(orient,[status(thm)],[t8403]) ).
cnf(t5894,plain,
multiply(inverse(multiply(sF0,multiply(inverse(X1),X1))),sF1) = multiply(inverse(sF1),multiply(inverse(sF1),b2)),
inference(cp,[status(thm)],[t5449,t5864]) ).
cnf(t8410,plain,
multiply(inverse(multiply(sF0,multiply(inverse(X1),X1))),sF1) = multiply(inverse(multiply(sF0,sF1)),sF1),
inference(step,[status(thm)],[t5894,t5449]) ).
cnf(t5896,plain,
multiply(inverse(multiply(sF0,multiply(inverse(X1),X1))),sF1) = multiply(inverse(multiply(sF0,sF1)),sF1),
inference(orient,[status(thm)],[t8410]) ).
cnf(t5912,plain,
multiply(inverse(X1),X1) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(sF0,sF1)),sF1))),inverse(multiply(b2,inverse(sF1))))),
inference(cp,[status(thm)],[t5714,t5896]) ).
cnf(t8416,plain,
multiply(inverse(X1),X1) = sF1,
inference(step,[status(thm)],[t5912,t5714]) ).
cnf(t5913,plain,
multiply(inverse(X1),X1) = sF1,
inference(orient,[status(thm)],[t8416]) ).
cnf(t6062,plain,
inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,sF1)))))),sF1)) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(rw,[status(thm)],[t5137]) ).
cnf(t289,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(multiply(X2,b2)),inverse(multiply(X1,inverse(multiply(multiply(X2,b2),inverse(multiply(inverse(multiply(X2,b2)),multiply(X2,b2))))))))),multiply(inverse(sF1),sF1)),
inference(cp,[status(thm)],[t273,t174]) ).
cnf(t8051,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(multiply(X2,b2)),inverse(multiply(X1,inverse(multiply(multiply(X2,b2),inverse(multiply(inverse(sF1),sF1)))))))),multiply(inverse(sF1),sF1)),
inference(step,[status(thm)],[t289,t174]) ).
cnf(t304,plain,
multiply(inverse(multiply(inverse(multiply(X1,b2)),inverse(multiply(X2,inverse(multiply(multiply(X1,b2),inverse(multiply(inverse(sF1),sF1)))))))),multiply(inverse(sF1),sF1)) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8051]) ).
cnf(t314,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X2,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),b2),inverse(multiply(inverse(sF1),sF1)))))))),multiply(inverse(sF1),sF1)),
inference(cp,[status(thm)],[t304,t308]) ).
cnf(t8244,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X2,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),b2),inverse(multiply(inverse(sF1),sF1)))))))),multiply(inverse(sF1),sF1)),
inference(step,[status(thm)],[t314,t24]) ).
cnf(t8245,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(inverse(sF1),sF1)))))))),multiply(inverse(sF1),sF1)),
inference(step,[status(thm)],[t8244,t308]) ).
cnf(t4443,plain,
multiply(inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(inverse(sF1),sF1)))))))),multiply(inverse(sF1),sF1)) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8245]) ).
cnf(t4448,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(X2))),inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(sF1),sF1)))))))),multiply(inverse(sF1),sF1)),
inference(cp,[status(thm)],[t4443,t31]) ).
cnf(t8247,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(X2),inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(sF1),sF1)))))))),multiply(inverse(sF1),sF1)),
inference(step,[status(thm)],[t4448,t31]) ).
cnf(t4482,plain,
multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(inverse(sF1),sF1)))))))),multiply(inverse(sF1),sF1)) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8247]) ).
cnf(t8373,plain,
multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(X1,inverse(sF1))))))),multiply(inverse(sF1),sF1)) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(step,[status(thm)],[t4482,t5354]) ).
cnf(t8374,plain,
multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(X1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(step,[status(thm)],[t8373,t5354]) ).
cnf(t5436,plain,
multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(X1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(rw,[status(thm)],[t8374]) ).
cnf(t5677,plain,
multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(X1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t5436]) ).
cnf(t5980,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(X1,inverse(sF1)))),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(X1),inverse(sF1))),sF1),
inference(cp,[status(thm)],[t5677,t5913]) ).
cnf(t8536,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(sF1))))),sF1))),inverse(multiply(b2,inverse(sF1)))) = multiply(inverse(multiply(inverse(X1),inverse(sF1))),sF1),
inference(step,[status(thm)],[t5980,t5136]) ).
cnf(t8537,plain,
multiply(X1,inverse(sF1)) = multiply(inverse(multiply(inverse(X1),inverse(sF1))),sF1),
inference(step,[status(thm)],[t8536,t5212]) ).
cnf(t6016,plain,
multiply(inverse(multiply(inverse(X1),inverse(sF1))),sF1) = multiply(X1,inverse(sF1)),
inference(orient,[status(thm)],[t8537]) ).
cnf(t6020,plain,
multiply(inverse(sF1),inverse(sF1)) = multiply(inverse(sF1),sF1),
inference(cp,[status(thm)],[t6016,t5913]) ).
cnf(t8538,plain,
multiply(inverse(sF1),inverse(sF1)) = sF1,
inference(step,[status(thm)],[t6020,t5913]) ).
cnf(t6023,plain,
multiply(inverse(sF1),inverse(sF1)) = sF1,
inference(orient,[status(thm)],[t8538]) ).
cnf(t6024,plain,
multiply(inverse(multiply(sF0,inverse(sF1))),sF1) = multiply(inverse(sF1),multiply(inverse(sF1),b2)),
inference(cp,[status(thm)],[t337,t6023]) ).
cnf(t5978,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))),sF1))),inverse(multiply(b2,inverse(sF1)))) = multiply(inverse(multiply(sF0,inverse(sF1))),sF1),
inference(cp,[status(thm)],[t5136,t5913]) ).
cnf(t8532,plain,
multiply(b2,inverse(sF1)) = multiply(inverse(multiply(sF0,inverse(sF1))),sF1),
inference(step,[status(thm)],[t5978,t5212]) ).
cnf(t5982,plain,
multiply(inverse(multiply(sF0,inverse(sF1))),sF1) = multiply(b2,inverse(sF1)),
inference(orient,[status(thm)],[t8532]) ).
cnf(t8541,plain,
multiply(b2,inverse(sF1)) = multiply(inverse(sF1),multiply(inverse(sF1),b2)),
inference(step,[status(thm)],[t6024,t5982]) ).
cnf(t8542,plain,
multiply(b2,inverse(sF1)) = multiply(inverse(multiply(sF0,sF1)),sF1),
inference(step,[status(thm)],[t8541,t5449]) ).
cnf(t6036,plain,
multiply(inverse(multiply(sF0,sF1)),sF1) = multiply(b2,inverse(sF1)),
inference(orient,[status(thm)],[t8542]) ).
cnf(t6059,plain,
sF1 = inverse(multiply(inverse(inverse(multiply(b2,inverse(sF1)))),inverse(multiply(b2,inverse(sF1))))),
inference(cp,[status(thm)],[t5714,t6036]) ).
cnf(t8553,plain,
sF1 = inverse(sF1),
inference(step,[status(thm)],[t6059,t5913]) ).
cnf(t6061,plain,
inverse(sF1) = sF1,
inference(orient,[status(thm)],[t8553]) ).
cnf(t8571,plain,
multiply(sF1,multiply(inverse(X1),b2)) = multiply(inverse(multiply(sF0,X1)),sF1),
inference(step,[status(thm)],[t5449,t6061]) ).
cnf(t6092,plain,
multiply(sF1,multiply(inverse(X1),b2)) = multiply(inverse(multiply(sF0,X1)),sF1),
inference(rw,[status(thm)],[t8571]) ).
cnf(t6130,plain,
multiply(inverse(multiply(sF0,X1)),sF1) = multiply(sF1,multiply(inverse(X1),b2)),
inference(orient,[status(thm)],[t6092]) ).
cnf(t8697,plain,
inverse(multiply(sF1,multiply(inverse(inverse(multiply(X1,inverse(multiply(b2,sF1))))),b2))) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t6062,t6130]) ).
cnf(t6102,plain,
multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(X1,sF1)))))),sF1) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(rw,[status(thm)],[t5677]) ).
cnf(t8650,plain,
multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(X1,sF1)))))),sF1) = multiply(sF1,multiply(inverse(inverse(multiply(X2,inverse(multiply(b2,inverse(sF1)))))),b2)),
inference(step,[status(thm)],[t6102,t6130]) ).
cnf(t8651,plain,
multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(X1,sF1)))))),sF1) = multiply(sF1,multiply(inverse(inverse(multiply(X2,inverse(multiply(b2,sF1))))),b2)),
inference(step,[status(thm)],[t8650,t6061]) ).
cnf(t6242,plain,
multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(X1,sF1)))))),sF1) = multiply(sF1,multiply(inverse(inverse(multiply(X2,inverse(multiply(b2,sF1))))),b2)),
inference(orient,[status(thm)],[t8651]) ).
cnf(t6244,plain,
multiply(sF1,multiply(inverse(inverse(multiply(X1,inverse(multiply(b2,sF1))))),b2)) = multiply(inverse(multiply(inverse(inverse(sF1)),inverse(multiply(X1,inverse(sF1))))),sF1),
inference(cp,[status(thm)],[t6242,t5913]) ).
cnf(t8652,plain,
multiply(sF1,multiply(inverse(inverse(multiply(X1,inverse(multiply(b2,sF1))))),b2)) = multiply(inverse(multiply(inverse(sF1),inverse(multiply(X1,inverse(sF1))))),sF1),
inference(step,[status(thm)],[t6244,t6061]) ).
cnf(t8653,plain,
multiply(sF1,multiply(inverse(inverse(multiply(X1,inverse(multiply(b2,sF1))))),b2)) = multiply(inverse(multiply(sF1,inverse(multiply(X1,inverse(sF1))))),sF1),
inference(step,[status(thm)],[t8652,t6061]) ).
cnf(t8654,plain,
multiply(sF1,multiply(inverse(inverse(multiply(X1,inverse(multiply(b2,sF1))))),b2)) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(step,[status(thm)],[t8653,t6061]) ).
cnf(t6261,plain,
multiply(sF1,multiply(inverse(inverse(multiply(X1,inverse(multiply(b2,sF1))))),b2)) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(orient,[status(thm)],[t8654]) ).
cnf(t8698,plain,
inverse(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1)) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,X1)),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t8697,t6261]) ).
cnf(t8699,plain,
inverse(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1)) = multiply(inverse(inverse(multiply(sF1,multiply(inverse(X1),b2)))),inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t8698,t6130]) ).
cnf(t8700,plain,
inverse(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1)) = multiply(inverse(inverse(multiply(sF1,multiply(inverse(X1),b2)))),inverse(multiply(b2,sF1))),
inference(step,[status(thm)],[t8699,t6061]) ).
cnf(t8378,plain,
multiply(inverse(inverse(multiply(inverse(sF1),multiply(X1,b2)))),inverse(multiply(b2,inverse(sF1)))) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(step,[status(thm)],[t5086,t5354]) ).
cnf(t5441,plain,
multiply(inverse(inverse(multiply(inverse(sF1),multiply(X1,b2)))),inverse(multiply(b2,inverse(sF1)))) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(rw,[status(thm)],[t8378]) ).
cnf(t5698,plain,
multiply(inverse(inverse(multiply(inverse(sF1),multiply(X1,b2)))),inverse(multiply(b2,inverse(sF1)))) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t5441]) ).
cnf(t6103,plain,
multiply(inverse(inverse(multiply(sF1,multiply(X1,b2)))),inverse(multiply(b2,sF1))) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(rw,[status(thm)],[t5698]) ).
cnf(t8672,plain,
multiply(inverse(inverse(multiply(sF1,multiply(X1,b2)))),inverse(multiply(b2,sF1))) = multiply(sF1,multiply(inverse(inverse(multiply(X1,inverse(multiply(b2,inverse(sF1)))))),b2)),
inference(step,[status(thm)],[t6103,t6130]) ).
cnf(t8673,plain,
multiply(inverse(inverse(multiply(sF1,multiply(X1,b2)))),inverse(multiply(b2,sF1))) = multiply(sF1,multiply(inverse(inverse(multiply(X1,inverse(multiply(b2,sF1))))),b2)),
inference(step,[status(thm)],[t8672,t6061]) ).
cnf(t8674,plain,
multiply(inverse(inverse(multiply(sF1,multiply(X1,b2)))),inverse(multiply(b2,sF1))) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(step,[status(thm)],[t8673,t6261]) ).
cnf(t6337,plain,
multiply(inverse(inverse(multiply(sF1,multiply(X1,b2)))),inverse(multiply(b2,sF1))) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(orient,[status(thm)],[t8674]) ).
cnf(t8701,plain,
inverse(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1)) = multiply(inverse(multiply(sF1,inverse(multiply(inverse(X1),sF1)))),sF1),
inference(step,[status(thm)],[t8700,t6337]) ).
cnf(t6404,plain,
inverse(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1)) = multiply(inverse(multiply(sF1,inverse(multiply(inverse(X1),sF1)))),sF1),
inference(orient,[status(thm)],[t8701]) ).
cnf(t4144,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(X3,inverse(multiply(inverse(sF1),sF1)))))))),multiply(X2,multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X3)),inverse(multiply(b2,inverse(sF1))))))),sF1))),
inference(cp,[status(thm)],[t4142,t31]) ).
cnf(t8227,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(X3,inverse(multiply(inverse(sF1),sF1)))))))),multiply(X2,X3)),
inference(step,[status(thm)],[t4144,t31]) ).
cnf(t4196,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(sF1),sF1)))))))),multiply(X1,X3)) = multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t8227]) ).
cnf(t3,axiom,
sF2 = multiply(multiply(inverse(b2),b2),a2),
introduced(definition) ).
cnf(t7982,plain,
sF2 = multiply(multiply(sF0,b2),a2),
inference(step,[status(thm)],[t3,t4]) ).
cnf(t7983,plain,
sF2 = multiply(sF1,a2),
inference(step,[status(thm)],[t7982,t5]) ).
cnf(t6,plain,
multiply(sF1,a2) = sF2,
inference(orient,[status(thm)],[t7983]) ).
cnf(t4200,plain,
multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(X1,inverse(multiply(a2,inverse(multiply(inverse(sF1),sF1)))))))),sF2),
inference(cp,[status(thm)],[t4196,t6]) ).
cnf(t4267,plain,
multiply(inverse(multiply(sF1,inverse(multiply(X1,inverse(multiply(a2,inverse(multiply(inverse(sF1),sF1)))))))),sF2) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t4200]) ).
cnf(t8368,plain,
multiply(inverse(multiply(sF1,inverse(multiply(X1,inverse(multiply(a2,inverse(sF1))))))),sF2) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(step,[status(thm)],[t4267,t5354]) ).
cnf(t5431,plain,
multiply(inverse(multiply(sF1,inverse(multiply(X1,inverse(multiply(a2,inverse(sF1))))))),sF2) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(rw,[status(thm)],[t8368]) ).
cnf(t5584,plain,
multiply(inverse(multiply(sF1,inverse(multiply(X1,inverse(multiply(a2,inverse(sF1))))))),sF2) = multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(orient,[status(thm)],[t5431]) ).
cnf(t5979,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(a2,inverse(sF1)))),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(sF1,inverse(sF1))),sF2),
inference(cp,[status(thm)],[t5584,t5913]) ).
cnf(t8533,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(a2,inverse(sF1))))),sF1))),inverse(multiply(b2,inverse(sF1)))) = multiply(inverse(multiply(sF1,inverse(sF1))),sF2),
inference(step,[status(thm)],[t5979,t5136]) ).
cnf(t8534,plain,
multiply(a2,inverse(sF1)) = multiply(inverse(multiply(sF1,inverse(sF1))),sF2),
inference(step,[status(thm)],[t8533,t5212]) ).
cnf(t5987,plain,
multiply(inverse(multiply(sF1,inverse(sF1))),sF2) = multiply(a2,inverse(sF1)),
inference(orient,[status(thm)],[t8534]) ).
cnf(t6027,plain,
multiply(sF1,inverse(sF1)) = multiply(inverse(sF1),sF1),
inference(cp,[status(thm)],[t6016,t6023]) ).
cnf(t8539,plain,
multiply(sF1,inverse(sF1)) = sF1,
inference(step,[status(thm)],[t6027,t5913]) ).
cnf(t6028,plain,
multiply(sF1,inverse(sF1)) = sF1,
inference(orient,[status(thm)],[t8539]) ).
cnf(t8540,plain,
multiply(inverse(sF1),sF2) = multiply(a2,inverse(sF1)),
inference(step,[status(thm)],[t5987,t6028]) ).
cnf(t6029,plain,
multiply(inverse(sF1),sF2) = multiply(a2,inverse(sF1)),
inference(rw,[status(thm)],[t8540]) ).
cnf(t6033,plain,
multiply(inverse(sF1),sF2) = multiply(a2,inverse(sF1)),
inference(orient,[status(thm)],[t6029]) ).
cnf(t6110,plain,
multiply(sF1,sF2) = multiply(a2,inverse(sF1)),
inference(rw,[status(thm)],[t6033]) ).
cnf(t8588,plain,
multiply(sF1,sF2) = multiply(a2,sF1),
inference(step,[status(thm)],[t6110,t6061]) ).
cnf(t6117,plain,
multiply(a2,sF1) = multiply(sF1,sF2),
inference(orient,[status(thm)],[t8588]) ).
cnf(t6405,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(a2),sF1)))),sF1) = inverse(multiply(inverse(multiply(sF1,inverse(multiply(sF1,sF2)))),sF1)),
inference(cp,[status(thm)],[t6404,t6117]) ).
cnf(t6107,plain,
multiply(inverse(multiply(inverse(X1),sF1)),sF1) = multiply(X1,inverse(sF1)),
inference(rw,[status(thm)],[t6016]) ).
cnf(t8601,plain,
multiply(inverse(multiply(inverse(X1),sF1)),sF1) = multiply(X1,sF1),
inference(step,[status(thm)],[t6107,t6061]) ).
cnf(t6151,plain,
multiply(inverse(multiply(inverse(X1),sF1)),sF1) = multiply(X1,sF1),
inference(orient,[status(thm)],[t8601]) ).
cnf(t6154,plain,
multiply(multiply(inverse(X1),sF1),sF1) = multiply(inverse(multiply(X1,sF1)),sF1),
inference(cp,[status(thm)],[t6151,t6151]) ).
cnf(t6156,plain,
multiply(inverse(multiply(X1,sF1)),sF1) = multiply(multiply(inverse(X1),sF1),sF1),
inference(orient,[status(thm)],[t6154]) ).
cnf(t6158,plain,
multiply(multiply(inverse(a2),sF1),sF1) = multiply(inverse(multiply(sF1,sF2)),sF1),
inference(cp,[status(thm)],[t6156,t6117]) ).
cnf(t6163,plain,
multiply(inverse(multiply(sF1,sF2)),sF1) = multiply(multiply(inverse(a2),sF1),sF1),
inference(orient,[status(thm)],[t6158]) ).
cnf(t6409,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,sF2))),sF1)))),sF1) = inverse(multiply(inverse(multiply(sF1,inverse(multiply(multiply(inverse(a2),sF1),sF1)))),sF1)),
inference(cp,[status(thm)],[t6404,t6163]) ).
cnf(t6245,plain,
multiply(sF1,multiply(inverse(inverse(multiply(X1,inverse(multiply(b2,sF1))))),b2)) = multiply(inverse(multiply(inverse(a2),inverse(multiply(X1,inverse(multiply(sF1,sF2)))))),sF1),
inference(cp,[status(thm)],[t6242,t6117]) ).
cnf(t8683,plain,
multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1) = multiply(inverse(multiply(inverse(a2),inverse(multiply(X1,inverse(multiply(sF1,sF2)))))),sF1),
inference(step,[status(thm)],[t6245,t6261]) ).
cnf(t6367,plain,
multiply(inverse(multiply(inverse(a2),inverse(multiply(X1,inverse(multiply(sF1,sF2)))))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(orient,[status(thm)],[t8683]) ).
cnf(t6368,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,sF2))),sF1)))),sF1) = multiply(inverse(multiply(inverse(a2),inverse(sF1))),sF1),
inference(cp,[status(thm)],[t6367,t5913]) ).
cnf(t8691,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,sF2))),sF1)))),sF1) = multiply(inverse(multiply(inverse(a2),sF1)),sF1),
inference(step,[status(thm)],[t6368,t6061]) ).
cnf(t8692,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,sF2))),sF1)))),sF1) = multiply(multiply(inverse(inverse(a2)),sF1),sF1),
inference(step,[status(thm)],[t8691,t6156]) ).
cnf(t8602,plain,
multiply(multiply(inverse(inverse(X1)),sF1),sF1) = multiply(X1,sF1),
inference(step,[status(thm)],[t6151,t6156]) ).
cnf(t6157,plain,
multiply(multiply(inverse(inverse(X1)),sF1),sF1) = multiply(X1,sF1),
inference(rw,[status(thm)],[t8602]) ).
cnf(t6169,plain,
multiply(multiply(inverse(inverse(X1)),sF1),sF1) = multiply(X1,sF1),
inference(orient,[status(thm)],[t6157]) ).
cnf(t8693,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,sF2))),sF1)))),sF1) = multiply(a2,sF1),
inference(step,[status(thm)],[t8692,t6169]) ).
cnf(t8694,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,sF2))),sF1)))),sF1) = multiply(sF1,sF2),
inference(step,[status(thm)],[t8693,t6117]) ).
cnf(t6390,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,sF2))),sF1)))),sF1) = multiply(sF1,sF2),
inference(orient,[status(thm)],[t8694]) ).
cnf(t8737,plain,
multiply(sF1,sF2) = inverse(multiply(inverse(multiply(sF1,inverse(multiply(multiply(inverse(a2),sF1),sF1)))),sF1)),
inference(step,[status(thm)],[t6409,t6390]) ).
cnf(t8738,plain,
multiply(sF1,sF2) = multiply(inverse(multiply(sF1,inverse(multiply(inverse(multiply(inverse(a2),sF1)),sF1)))),sF1),
inference(step,[status(thm)],[t8737,t6404]) ).
cnf(t8739,plain,
multiply(sF1,sF2) = multiply(inverse(multiply(sF1,inverse(multiply(multiply(inverse(inverse(a2)),sF1),sF1)))),sF1),
inference(step,[status(thm)],[t8738,t6156]) ).
cnf(t8740,plain,
multiply(sF1,sF2) = multiply(inverse(multiply(sF1,inverse(multiply(a2,sF1)))),sF1),
inference(step,[status(thm)],[t8739,t6169]) ).
cnf(t8741,plain,
multiply(sF1,sF2) = multiply(inverse(multiply(sF1,inverse(multiply(sF1,sF2)))),sF1),
inference(step,[status(thm)],[t8740,t6117]) ).
cnf(t6494,plain,
multiply(inverse(multiply(sF1,inverse(multiply(sF1,sF2)))),sF1) = multiply(sF1,sF2),
inference(orient,[status(thm)],[t8741]) ).
cnf(t8754,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(a2),sF1)))),sF1) = inverse(multiply(sF1,sF2)),
inference(step,[status(thm)],[t6405,t6494]) ).
cnf(t6521,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(a2),sF1)))),sF1) = inverse(multiply(sF1,sF2)),
inference(orient,[status(thm)],[t8754]) ).
cnf(t6528,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(a2)),sF1)))),sF1) = inverse(inverse(multiply(sF1,sF2))),
inference(cp,[status(thm)],[t6404,t6521]) ).
cnf(t6638,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(a2)),sF1)))),sF1) = inverse(inverse(multiply(sF1,sF2))),
inference(orient,[status(thm)],[t6528]) ).
cnf(t8570,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(X1))),sF1))),inverse(multiply(b2,sF1))) = X1,
inference(step,[status(thm)],[t5212,t6061]) ).
cnf(t6091,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(X1))),sF1))),inverse(multiply(b2,sF1))) = X1,
inference(rw,[status(thm)],[t8570]) ).
cnf(t9149,plain,
multiply(inverse(inverse(multiply(sF1,multiply(inverse(inverse(X1)),b2)))),inverse(multiply(b2,sF1))) = X1,
inference(step,[status(thm)],[t6091,t6130]) ).
cnf(t164,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))))),inverse(multiply(b2,inverse(sF1))))))),sF1) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),sF1)),
inference(cp,[status(thm)],[t24,t163]) ).
cnf(t8026,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),sF1)),
inference(step,[status(thm)],[t164,t31]) ).
cnf(t8027,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(sF0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),sF1))),sF1)),
inference(step,[status(thm)],[t8026,t24]) ).
cnf(t8028,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(sF0,b2)),sF1)),
inference(step,[status(thm)],[t8027,t29]) ).
cnf(t8029,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(sF1),sF1)),
inference(step,[status(thm)],[t8028,t5]) ).
cnf(t194,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(sF1),sF1)),
inference(orient,[status(thm)],[t8029]) ).
cnf(t196,plain,
multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(inverse(multiply(inverse(sF1),sF1))),multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1))))),inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(cp,[status(thm)],[t150,t194]) ).
cnf(t8033,plain,
multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t196,t31]) ).
cnf(t222,plain,
multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(b2,inverse(sF1)))),
inference(orient,[status(thm)],[t8033]) ).
cnf(t8295,plain,
multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t222,t5354]) ).
cnf(t5355,plain,
multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1)))),
inference(orient,[status(thm)],[t8295]) ).
cnf(t6063,plain,
multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,sF1)))))),sF1) = multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1)))),
inference(rw,[status(thm)],[t5355]) ).
cnf(t8627,plain,
multiply(sF1,multiply(inverse(inverse(multiply(sF0,inverse(multiply(b2,sF1))))),b2)) = multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t6063,t6130]) ).
cnf(t8628,plain,
multiply(sF1,multiply(inverse(inverse(multiply(sF0,inverse(multiply(b2,sF1))))),b2)) = multiply(inverse(sF1),inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t8627,t6061]) ).
cnf(t8629,plain,
multiply(sF1,multiply(inverse(inverse(multiply(sF0,inverse(multiply(b2,sF1))))),b2)) = multiply(sF1,inverse(multiply(b2,inverse(sF1)))),
inference(step,[status(thm)],[t8628,t6061]) ).
cnf(t8630,plain,
multiply(sF1,multiply(inverse(inverse(multiply(sF0,inverse(multiply(b2,sF1))))),b2)) = multiply(sF1,inverse(multiply(b2,sF1))),
inference(step,[status(thm)],[t8629,t6061]) ).
cnf(t6202,plain,
multiply(sF1,multiply(inverse(inverse(multiply(sF0,inverse(multiply(b2,sF1))))),b2)) = multiply(sF1,inverse(multiply(b2,sF1))),
inference(orient,[status(thm)],[t8630]) ).
cnf(t8655,plain,
multiply(inverse(multiply(sF1,inverse(multiply(sF0,sF1)))),sF1) = multiply(sF1,inverse(multiply(b2,sF1))),
inference(step,[status(thm)],[t6202,t6261]) ).
cnf(t6262,plain,
multiply(inverse(multiply(sF1,inverse(multiply(sF0,sF1)))),sF1) = multiply(sF1,inverse(multiply(b2,sF1))),
inference(rw,[status(thm)],[t8655]) ).
cnf(t6271,plain,
multiply(inverse(multiply(sF1,inverse(multiply(sF0,sF1)))),sF1) = multiply(sF1,inverse(multiply(b2,sF1))),
inference(orient,[status(thm)],[t6262]) ).
cnf(t6273,plain,
multiply(multiply(inverse(inverse(multiply(sF1,inverse(multiply(sF0,sF1))))),sF1),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(b2,sF1)))),sF1),
inference(cp,[status(thm)],[t6156,t6271]) ).
cnf(t8660,plain,
multiply(multiply(sF1,inverse(multiply(sF0,sF1))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(b2,sF1)))),sF1),
inference(step,[status(thm)],[t6273,t6169]) ).
cnf(t234,plain,
multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF0),inverse(multiply(b2,inverse(sF1))))))),sF1) = inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(b2,inverse(sF1))))),
inference(cp,[status(thm)],[t24,t222]) ).
cnf(t8045,plain,
b2 = inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(b2,inverse(sF1))))),
inference(step,[status(thm)],[t234,t29]) ).
cnf(t238,plain,
inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(b2,inverse(sF1))))) = b2,
inference(orient,[status(thm)],[t8045]) ).
cnf(t8297,plain,
inverse(multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1))))) = b2,
inference(step,[status(thm)],[t238,t5354]) ).
cnf(t5357,plain,
inverse(multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1))))) = b2,
inference(rw,[status(thm)],[t8297]) ).
cnf(t5470,plain,
inverse(multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1))))) = b2,
inference(orient,[status(thm)],[t5357]) ).
cnf(t8572,plain,
inverse(multiply(inverse(sF1),inverse(multiply(b2,inverse(sF1))))) = b2,
inference(step,[status(thm)],[t5470,t6061]) ).
cnf(t8573,plain,
inverse(multiply(sF1,inverse(multiply(b2,inverse(sF1))))) = b2,
inference(step,[status(thm)],[t8572,t6061]) ).
cnf(t8574,plain,
inverse(multiply(sF1,inverse(multiply(b2,sF1)))) = b2,
inference(step,[status(thm)],[t8573,t6061]) ).
cnf(t6093,plain,
inverse(multiply(sF1,inverse(multiply(b2,sF1)))) = b2,
inference(rw,[status(thm)],[t8574]) ).
cnf(t6149,plain,
inverse(multiply(sF1,inverse(multiply(b2,sF1)))) = b2,
inference(orient,[status(thm)],[t6093]) ).
cnf(t8661,plain,
multiply(multiply(sF1,inverse(multiply(sF0,sF1))),sF1) = multiply(b2,sF1),
inference(step,[status(thm)],[t8660,t6149]) ).
cnf(t6276,plain,
multiply(multiply(sF1,inverse(multiply(sF0,sF1))),sF1) = multiply(b2,sF1),
inference(orient,[status(thm)],[t8661]) ).
cnf(t6416,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(multiply(sF1,inverse(multiply(sF0,sF1)))),sF1)))),sF1) = inverse(multiply(inverse(multiply(sF1,inverse(multiply(b2,sF1)))),sF1)),
inference(cp,[status(thm)],[t6404,t6276]) ).
cnf(t8717,plain,
multiply(inverse(multiply(sF1,multiply(inverse(multiply(sF1,inverse(multiply(inverse(sF0),sF1)))),sF1))),sF1) = inverse(multiply(inverse(multiply(sF1,inverse(multiply(b2,sF1)))),sF1)),
inference(step,[status(thm)],[t6416,t6404]) ).
cnf(t8269,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,sF0)),sF1))),inverse(multiply(b2,inverse(sF1)))) = b2,
inference(step,[status(thm)],[t29,t5136]) ).
cnf(t5139,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,sF0)),sF1))),inverse(multiply(b2,inverse(sF1)))) = b2,
inference(rw,[status(thm)],[t8269]) ).
cnf(t5181,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,sF0)),sF1))),inverse(multiply(b2,inverse(sF1)))) = b2,
inference(orient,[status(thm)],[t5139]) ).
cnf(t8565,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,sF0)),sF1))),inverse(multiply(b2,sF1))) = b2,
inference(step,[status(thm)],[t5181,t6061]) ).
cnf(t6088,plain,
multiply(inverse(inverse(multiply(inverse(multiply(sF0,sF0)),sF1))),inverse(multiply(b2,sF1))) = b2,
inference(rw,[status(thm)],[t8565]) ).
cnf(t8649,plain,
multiply(inverse(inverse(multiply(sF1,multiply(inverse(sF0),b2)))),inverse(multiply(b2,sF1))) = b2,
inference(step,[status(thm)],[t6088,t6130]) ).
cnf(t6241,plain,
multiply(inverse(inverse(multiply(sF1,multiply(inverse(sF0),b2)))),inverse(multiply(b2,sF1))) = b2,
inference(orient,[status(thm)],[t8649]) ).
cnf(t8675,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(sF0),sF1)))),sF1) = b2,
inference(step,[status(thm)],[t6241,t6337]) ).
cnf(t6338,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(sF0),sF1)))),sF1) = b2,
inference(rw,[status(thm)],[t8675]) ).
cnf(t6347,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(sF0),sF1)))),sF1) = b2,
inference(orient,[status(thm)],[t6338]) ).
cnf(t8718,plain,
multiply(inverse(multiply(sF1,b2)),sF1) = inverse(multiply(inverse(multiply(sF1,inverse(multiply(b2,sF1)))),sF1)),
inference(step,[status(thm)],[t8717,t6347]) ).
cnf(t8719,plain,
multiply(inverse(multiply(sF1,b2)),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(inverse(b2),sF1)))),sF1),
inference(step,[status(thm)],[t8718,t6404]) ).
cnf(t8720,plain,
multiply(inverse(multiply(sF1,b2)),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(sF0,sF1)))),sF1),
inference(step,[status(thm)],[t8719,t4]) ).
cnf(t6407,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(b2),sF1)))),sF1) = inverse(multiply(b2,sF1)),
inference(cp,[status(thm)],[t6404,t6149]) ).
cnf(t8702,plain,
multiply(inverse(multiply(sF1,inverse(multiply(sF0,sF1)))),sF1) = inverse(multiply(b2,sF1)),
inference(step,[status(thm)],[t6407,t4]) ).
cnf(t8703,plain,
multiply(sF1,inverse(multiply(b2,sF1))) = inverse(multiply(b2,sF1)),
inference(step,[status(thm)],[t8702,t6271]) ).
cnf(t6443,plain,
multiply(sF1,inverse(multiply(b2,sF1))) = inverse(multiply(b2,sF1)),
inference(orient,[status(thm)],[t8703]) ).
cnf(t8707,plain,
multiply(inverse(multiply(sF1,inverse(multiply(sF0,sF1)))),sF1) = inverse(multiply(b2,sF1)),
inference(step,[status(thm)],[t6271,t6443]) ).
cnf(t6448,plain,
multiply(inverse(multiply(sF1,inverse(multiply(sF0,sF1)))),sF1) = inverse(multiply(b2,sF1)),
inference(orient,[status(thm)],[t8707]) ).
cnf(t8721,plain,
multiply(inverse(multiply(sF1,b2)),sF1) = inverse(multiply(b2,sF1)),
inference(step,[status(thm)],[t8720,t6448]) ).
cnf(t6471,plain,
multiply(inverse(multiply(sF1,b2)),sF1) = inverse(multiply(b2,sF1)),
inference(orient,[status(thm)],[t8721]) ).
cnf(t6477,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,b2))),sF1)))),sF1) = inverse(multiply(inverse(multiply(sF1,inverse(inverse(multiply(b2,sF1))))),sF1)),
inference(cp,[status(thm)],[t6404,t6471]) ).
cnf(t8704,plain,
inverse(inverse(multiply(b2,sF1))) = b2,
inference(step,[status(thm)],[t6149,t6443]) ).
cnf(t6444,plain,
inverse(inverse(multiply(b2,sF1))) = b2,
inference(rw,[status(thm)],[t8704]) ).
cnf(t6454,plain,
inverse(inverse(multiply(b2,sF1))) = b2,
inference(orient,[status(thm)],[t6444]) ).
cnf(t8944,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,b2))),sF1)))),sF1) = inverse(multiply(inverse(multiply(sF1,b2)),sF1)),
inference(step,[status(thm)],[t6477,t6454]) ).
cnf(t8945,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,b2))),sF1)))),sF1) = inverse(inverse(multiply(b2,sF1))),
inference(step,[status(thm)],[t8944,t6471]) ).
cnf(t8946,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,b2))),sF1)))),sF1) = b2,
inference(step,[status(thm)],[t8945,t6454]) ).
cnf(t7065,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,b2))),sF1)))),sF1) = b2,
inference(orient,[status(thm)],[t8946]) ).
cnf(t7067,plain,
multiply(multiply(inverse(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,b2))),sF1))))),sF1),sF1) = multiply(inverse(b2),sF1),
inference(cp,[status(thm)],[t6156,t7065]) ).
cnf(t8947,plain,
multiply(multiply(sF1,inverse(multiply(inverse(inverse(multiply(sF1,b2))),sF1))),sF1) = multiply(inverse(b2),sF1),
inference(step,[status(thm)],[t7067,t6169]) ).
cnf(t6432,plain,
multiply(multiply(inverse(inverse(multiply(sF1,inverse(multiply(X1,sF1))))),sF1),sF1) = multiply(multiply(inverse(multiply(sF1,inverse(multiply(inverse(X1),sF1)))),sF1),sF1),
inference(cp,[status(thm)],[t6156,t6404]) ).
cnf(t8815,plain,
multiply(multiply(sF1,inverse(multiply(X1,sF1))),sF1) = multiply(multiply(inverse(multiply(sF1,inverse(multiply(inverse(X1),sF1)))),sF1),sF1),
inference(step,[status(thm)],[t6432,t6169]) ).
cnf(t6433,plain,
multiply(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),sF1) = multiply(multiply(inverse(multiply(inverse(multiply(sF1,inverse(multiply(inverse(X1),sF1)))),sF1)),sF1),sF1),
inference(cp,[status(thm)],[t6169,t6404]) ).
cnf(t8760,plain,
multiply(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),sF1) = multiply(multiply(multiply(inverse(inverse(multiply(sF1,inverse(multiply(inverse(X1),sF1))))),sF1),sF1),sF1),
inference(step,[status(thm)],[t6433,t6156]) ).
cnf(t8761,plain,
multiply(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),sF1) = multiply(multiply(multiply(sF1,inverse(multiply(inverse(X1),sF1))),sF1),sF1),
inference(step,[status(thm)],[t8760,t6169]) ).
cnf(t6558,plain,
multiply(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),sF1) = multiply(multiply(multiply(sF1,inverse(multiply(inverse(X1),sF1))),sF1),sF1),
inference(orient,[status(thm)],[t8761]) ).
cnf(t6604,plain,
multiply(multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),sF1) = multiply(multiply(multiply(inverse(inverse(X1)),sF1),sF1),sF1),
inference(orient,[status(thm)],[t6558]) ).
cnf(t8816,plain,
multiply(multiply(sF1,inverse(multiply(X1,sF1))),sF1) = multiply(multiply(multiply(inverse(inverse(inverse(X1))),sF1),sF1),sF1),
inference(step,[status(thm)],[t8815,t6604]) ).
cnf(t8817,plain,
multiply(multiply(sF1,inverse(multiply(X1,sF1))),sF1) = multiply(multiply(inverse(X1),sF1),sF1),
inference(step,[status(thm)],[t8816,t6169]) ).
cnf(t6702,plain,
multiply(multiply(sF1,inverse(multiply(X1,sF1))),sF1) = multiply(multiply(inverse(X1),sF1),sF1),
inference(orient,[status(thm)],[t8817]) ).
cnf(t8948,plain,
multiply(multiply(inverse(inverse(inverse(multiply(sF1,b2)))),sF1),sF1) = multiply(inverse(b2),sF1),
inference(step,[status(thm)],[t8947,t6702]) ).
cnf(t8949,plain,
multiply(inverse(multiply(sF1,b2)),sF1) = multiply(inverse(b2),sF1),
inference(step,[status(thm)],[t8948,t6169]) ).
cnf(t8950,plain,
inverse(multiply(b2,sF1)) = multiply(inverse(b2),sF1),
inference(step,[status(thm)],[t8949,t6471]) ).
cnf(t8951,plain,
inverse(multiply(b2,sF1)) = multiply(sF0,sF1),
inference(step,[status(thm)],[t8950,t4]) ).
cnf(t7074,plain,
inverse(multiply(b2,sF1)) = multiply(sF0,sF1),
inference(orient,[status(thm)],[t8951]) ).
cnf(t9150,plain,
multiply(inverse(inverse(multiply(sF1,multiply(inverse(inverse(X1)),b2)))),multiply(sF0,sF1)) = X1,
inference(step,[status(thm)],[t9149,t7074]) ).
cnf(t8964,plain,
multiply(inverse(inverse(multiply(sF1,multiply(X1,b2)))),multiply(sF0,sF1)) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(step,[status(thm)],[t6337,t7074]) ).
cnf(t7086,plain,
multiply(inverse(inverse(multiply(sF1,multiply(X1,b2)))),multiply(sF0,sF1)) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(rw,[status(thm)],[t8964]) ).
cnf(t7243,plain,
multiply(inverse(inverse(multiply(sF1,multiply(X1,b2)))),multiply(sF0,sF1)) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(orient,[status(thm)],[t7086]) ).
cnf(t9151,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(X1)),sF1)))),sF1) = X1,
inference(step,[status(thm)],[t9150,t7243]) ).
cnf(t7612,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(X1)),sF1)))),sF1) = X1,
inference(orient,[status(thm)],[t9151]) ).
cnf(t9153,plain,
a2 = inverse(inverse(multiply(sF1,sF2))),
inference(step,[status(thm)],[t6638,t7612]) ).
cnf(t7614,plain,
a2 = inverse(inverse(multiply(sF1,sF2))),
inference(rw,[status(thm)],[t9153]) ).
cnf(t7838,plain,
inverse(inverse(multiply(sF1,sF2))) = a2,
inference(orient,[status(thm)],[t7614]) ).
cnf(t6408,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(X1,sF1))),sF1)))),sF1) = inverse(multiply(inverse(multiply(sF1,inverse(multiply(multiply(inverse(X1),sF1),sF1)))),sF1)),
inference(cp,[status(thm)],[t6404,t6156]) ).
cnf(t8913,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(X1,sF1))),sF1)))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(inverse(multiply(inverse(X1),sF1)),sF1)))),sF1),
inference(step,[status(thm)],[t6408,t6404]) ).
cnf(t8914,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(X1,sF1))),sF1)))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(multiply(inverse(inverse(X1)),sF1),sF1)))),sF1),
inference(step,[status(thm)],[t8913,t6156]) ).
cnf(t8915,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(X1,sF1))),sF1)))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(step,[status(thm)],[t8914,t6169]) ).
cnf(t6980,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(multiply(X1,sF1))),sF1)))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(X1,sF1)))),sF1),
inference(orient,[status(thm)],[t8915]) ).
cnf(t6982,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(multiply(sF1,inverse(multiply(inverse(a2),sF1)))),sF1)))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(inverse(multiply(sF1,sF2)))),sF1)))),sF1),
inference(cp,[status(thm)],[t6980,t6521]) ).
cnf(t8928,plain,
multiply(inverse(multiply(sF1,multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(a2)),sF1)))),sF1))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(inverse(multiply(sF1,sF2)))),sF1)))),sF1),
inference(step,[status(thm)],[t6982,t6404]) ).
cnf(t8929,plain,
multiply(inverse(multiply(sF1,inverse(inverse(multiply(sF1,sF2))))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(inverse(multiply(sF1,sF2)))),sF1)))),sF1),
inference(step,[status(thm)],[t8928,t6638]) ).
cnf(t6640,plain,
multiply(multiply(inverse(inverse(multiply(sF1,inverse(multiply(inverse(inverse(a2)),sF1))))),sF1),sF1) = multiply(inverse(inverse(inverse(multiply(sF1,sF2)))),sF1),
inference(cp,[status(thm)],[t6156,t6638]) ).
cnf(t8795,plain,
multiply(multiply(sF1,inverse(multiply(inverse(inverse(a2)),sF1))),sF1) = multiply(inverse(inverse(inverse(multiply(sF1,sF2)))),sF1),
inference(step,[status(thm)],[t6640,t6169]) ).
cnf(t6664,plain,
multiply(multiply(sF1,inverse(multiply(inverse(inverse(a2)),sF1))),sF1) = multiply(inverse(inverse(inverse(multiply(sF1,sF2)))),sF1),
inference(orient,[status(thm)],[t8795]) ).
cnf(t6717,plain,
multiply(multiply(inverse(inverse(inverse(a2))),sF1),sF1) = multiply(inverse(inverse(inverse(multiply(sF1,sF2)))),sF1),
inference(rw,[status(thm)],[t6664]) ).
cnf(t8835,plain,
multiply(inverse(a2),sF1) = multiply(inverse(inverse(inverse(multiply(sF1,sF2)))),sF1),
inference(step,[status(thm)],[t6717,t6169]) ).
cnf(t6746,plain,
multiply(inverse(inverse(inverse(multiply(sF1,sF2)))),sF1) = multiply(inverse(a2),sF1),
inference(orient,[status(thm)],[t8835]) ).
cnf(t8930,plain,
multiply(inverse(multiply(sF1,inverse(inverse(multiply(sF1,sF2))))),sF1) = multiply(inverse(multiply(sF1,inverse(multiply(inverse(a2),sF1)))),sF1),
inference(step,[status(thm)],[t8929,t6746]) ).
cnf(t8931,plain,
multiply(inverse(multiply(sF1,inverse(inverse(multiply(sF1,sF2))))),sF1) = inverse(multiply(sF1,sF2)),
inference(step,[status(thm)],[t8930,t6521]) ).
cnf(t7015,plain,
multiply(inverse(multiply(sF1,inverse(inverse(multiply(sF1,sF2))))),sF1) = inverse(multiply(sF1,sF2)),
inference(orient,[status(thm)],[t8931]) ).
cnf(t7848,plain,
multiply(inverse(multiply(sF1,a2)),sF1) = inverse(multiply(sF1,sF2)),
inference(rw,[status(thm)],[t7015]) ).
cnf(t9337,plain,
multiply(inverse(sF2),sF1) = inverse(multiply(sF1,sF2)),
inference(step,[status(thm)],[t7848,t6]) ).
cnf(t7931,plain,
inverse(multiply(sF1,sF2)) = multiply(inverse(sF2),sF1),
inference(orient,[status(thm)],[t9337]) ).
cnf(t9347,plain,
inverse(multiply(inverse(sF2),sF1)) = a2,
inference(step,[status(thm)],[t7838,t7931]) ).
cnf(t7941,plain,
inverse(multiply(inverse(sF2),sF1)) = a2,
inference(rw,[status(thm)],[t9347]) ).
cnf(t7953,plain,
inverse(multiply(inverse(sF2),sF1)) = a2,
inference(orient,[status(thm)],[t7941]) ).
cnf(t7964,plain,
multiply(inverse(multiply(sF1,inverse(multiply(inverse(inverse(sF2)),sF1)))),sF1) = inverse(multiply(inverse(multiply(sF1,a2)),sF1)),
inference(cp,[status(thm)],[t6404,t7953]) ).
cnf(t9348,plain,
sF2 = inverse(multiply(inverse(multiply(sF1,a2)),sF1)),
inference(step,[status(thm)],[t7964,t7612]) ).
cnf(t9349,plain,
sF2 = inverse(multiply(inverse(sF2),sF1)),
inference(step,[status(thm)],[t9348,t6]) ).
cnf(t9350,plain,
sF2 = a2,
inference(step,[status(thm)],[t9349,t7953]) ).
cnf(t7970,plain,
a2 = sF2,
inference(orient,[status(thm)],[t9350]) ).
cnf(t9351,plain,
multiply(sF1,sF2) = sF2,
inference(step,[status(thm)],[t6,t7970]) ).
cnf(t7971,plain,
multiply(sF1,sF2) = sF2,
inference(rw,[status(thm)],[t9351]) ).
cnf(t7977,plain,
multiply(sF1,sF2) = sF2,
inference(orient,[status(thm)],[t7971]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(sF1,a2) != a2,
inference(rw,[status(thm)],[goal_0,t5913]) ).
cnf(g0_1,plain,
multiply(sF1,sF2) != a2,
inference(rw,[status(thm)],[g0_0,t7970]) ).
cnf(g0_2,plain,
sF2 != a2,
inference(rw,[status(thm)],[g0_1,t7977]) ).
cnf(g0_3,plain,
sF2 != sF2,
inference(rw,[status(thm)],[g0_2,t7970]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP419-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n001.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 14:48:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 35.49/5.33 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.49/5.33 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------