%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP411-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 : n008.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:06 PM UTC 2026
% Result : Unsatisfiable 14.26s 7.73s
% Output : CNFRefutation 14.26s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),inverse(multiply(inverse(X3),X3))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,plain,
multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),inverse(multiply(inverse(X3),X3))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t3,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))) = multiply(multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t81,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))) = multiply(multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(orient,[status(thm)],[t3]) ).
cnf(t135,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(Y3,inverse(multiply(X2,X3)))),multiply(Y3,inverse(X3))),
inference(cp,[status(thm)],[t81,t81]) ).
cnf(t157,plain,
multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(Y3,inverse(multiply(X2,X3)))),multiply(Y3,inverse(X3))),
inference(orient,[status(thm)],[t135]) ).
cnf(t110,plain,
multiply(inverse(multiply(X1,inverse(multiply(multiply(X2,inverse(multiply(inverse(X3),X3))),X3)))),multiply(X1,inverse(X3))) = X2,
inference(cp,[status(thm)],[t81,t1]) ).
cnf(t136,plain,
multiply(inverse(multiply(X1,inverse(multiply(multiply(X2,inverse(multiply(inverse(X3),X3))),X3)))),multiply(X1,inverse(X3))) = X2,
inference(orient,[status(thm)],[t110]) ).
cnf(t165,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X2,inverse(multiply(multiply(X3,inverse(multiply(inverse(Y3),Y3))),Y3)))),multiply(X2,inverse(Y3)))))),multiply(X1,inverse(multiply(X2,inverse(Y3))))) = multiply(inverse(multiply(Y4,inverse(X3))),multiply(Y4,inverse(multiply(X2,inverse(Y3))))),
inference(cp,[status(thm)],[t157,t136]) ).
cnf(t25555,plain,
multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(multiply(X2,inverse(Y3))))) = multiply(inverse(multiply(Y4,inverse(X3))),multiply(Y4,inverse(multiply(X2,inverse(Y3))))),
inference(step,[status(thm)],[t165,t136]) ).
cnf(t189,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(X3,inverse(Y3))))) = multiply(inverse(multiply(Y4,inverse(X2))),multiply(Y4,inverse(multiply(X3,inverse(Y3))))),
inference(orient,[status(thm)],[t25555]) ).
cnf(t205,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(multiply(Y3,Y4)))),multiply(X3,inverse(Y4))),inverse(multiply(inverse(Y4),Y4)))))) = multiply(inverse(multiply(Y5,inverse(X2))),multiply(Y5,inverse(Y3))),
inference(cp,[status(thm)],[t189,t1]) ).
cnf(t25556,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(Y3))) = multiply(inverse(multiply(Y5,inverse(X2))),multiply(Y5,inverse(Y3))),
inference(step,[status(thm)],[t205,t1]) ).
cnf(t233,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,inverse(X3))),
inference(orient,[status(thm)],[t25556]) ).
cnf(t248,plain,
X1 = multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X3,inverse(Y3)))))),multiply(X2,inverse(multiply(X3,inverse(Y3))))),inverse(multiply(inverse(multiply(Y4,inverse(Y3))),multiply(Y4,inverse(Y3))))),
inference(cp,[status(thm)],[t1,t233]) ).
cnf(t268,plain,
multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(X3,inverse(Y3)))))),multiply(X1,inverse(multiply(X3,inverse(Y3))))),inverse(multiply(inverse(multiply(Y4,inverse(Y3))),multiply(Y4,inverse(Y3))))) = X2,
inference(orient,[status(thm)],[t248]) ).
cnf(t281,plain,
X1 = multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(multiply(multiply(inverse(multiply(Y3,inverse(multiply(X3,Y4)))),multiply(Y3,inverse(Y4))),inverse(multiply(inverse(Y4),Y4)))))),inverse(multiply(inverse(multiply(Y5,inverse(multiply(inverse(Y4),Y4)))),multiply(Y5,inverse(multiply(inverse(Y4),Y4)))))),
inference(cp,[status(thm)],[t268,t1]) ).
cnf(t25557,plain,
X1 = multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(multiply(inverse(multiply(Y5,inverse(multiply(inverse(Y4),Y4)))),multiply(Y5,inverse(multiply(inverse(Y4),Y4)))))),
inference(step,[status(thm)],[t281,t1]) ).
cnf(t391,plain,
multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),inverse(multiply(inverse(multiply(Y3,inverse(multiply(inverse(Y4),Y4)))),multiply(Y3,inverse(multiply(inverse(Y4),Y4)))))) = X2,
inference(orient,[status(thm)],[t25557]) ).
cnf(t422,plain,
X1 = multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(multiply(inverse(Y3),multiply(multiply(inverse(multiply(Y4,inverse(multiply(Y3,Y5)))),multiply(Y4,inverse(Y5))),inverse(multiply(inverse(Y5),Y5)))))),
inference(cp,[status(thm)],[t391,t1]) ).
cnf(t25558,plain,
X1 = multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(multiply(inverse(Y3),Y3))),
inference(step,[status(thm)],[t422,t1]) ).
cnf(t478,plain,
multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),inverse(multiply(inverse(Y3),Y3))) = X2,
inference(orient,[status(thm)],[t25558]) ).
cnf(t479,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(X1,inverse(multiply(inverse(X3),X3))),
inference(cp,[status(thm)],[t478,t136]) ).
cnf(t534,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(X1,inverse(multiply(inverse(X3),X3))),
inference(orient,[status(thm)],[t479]) ).
cnf(t539,plain,
inverse(X1) = multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),multiply(X2,inverse(X1))),inverse(multiply(inverse(Y3),Y3))),
inference(cp,[status(thm)],[t478,t534]) ).
cnf(t1072,plain,
multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(X3))),inverse(multiply(inverse(Y3),Y3))) = inverse(X3),
inference(orient,[status(thm)],[t539]) ).
cnf(t549,plain,
X1 = multiply(inverse(multiply(X2,inverse(multiply(multiply(X1,inverse(multiply(inverse(X3),X3))),Y3)))),multiply(X2,inverse(Y3))),
inference(cp,[status(thm)],[t136,t534]) ).
cnf(t1030,plain,
multiply(inverse(multiply(X1,inverse(multiply(multiply(X2,inverse(multiply(inverse(X3),X3))),Y3)))),multiply(X1,inverse(Y3))) = X2,
inference(orient,[status(thm)],[t549]) ).
cnf(t2,plain,
inverse(X1) = multiply(multiply(inverse(X2),multiply(multiply(inverse(multiply(X3,inverse(multiply(X2,X1)))),multiply(X3,inverse(X1))),inverse(X1))),inverse(multiply(inverse(X1),X1))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t5,plain,
multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))),inverse(multiply(inverse(X3),X3))) = inverse(X3),
inference(orient,[status(thm)],[t2]) ).
cnf(t504,plain,
inverse(multiply(inverse(X1),X1)) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))),
inference(cp,[status(thm)],[t5,t478]) ).
cnf(t25559,plain,
inverse(multiply(inverse(X1),X1)) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(c3),c3))),
inference(step,[status(thm)],[t504,t534]) ).
cnf(t572,plain,
inverse(multiply(inverse(X1),X1)) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t25559]) ).
cnf(t619,plain,
inverse(multiply(inverse(X1),X1)) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),X3))),
inference(cp,[status(thm)],[t572,t534]) ).
cnf(t690,plain,
inverse(multiply(inverse(X1),X1)) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),X3))),
inference(orient,[status(thm)],[t619]) ).
cnf(t1041,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X3),X3)),Y3)))),multiply(X2,inverse(Y3))),
inference(cp,[status(thm)],[t1030,t690]) ).
cnf(t1137,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X3),X3)),Y3)))),multiply(X2,inverse(Y3))),
inference(orient,[status(thm)],[t1041]) ).
cnf(t1201,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(multiply(inverse(multiply(X3,inverse(multiply(X2,Y3)))),multiply(X3,inverse(Y3))),inverse(multiply(inverse(Y4),Y4)))),
inference(cp,[status(thm)],[t1137,t478]) ).
cnf(t25560,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(step,[status(thm)],[t1201,t478]) ).
cnf(t1250,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t25560]) ).
cnf(t1264,plain,
inverse(X1) = multiply(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),multiply(inverse(X3),X3)),inverse(multiply(inverse(Y3),Y3))),
inference(cp,[status(thm)],[t1072,t1250]) ).
cnf(t4339,plain,
multiply(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),multiply(inverse(X3),X3)),inverse(multiply(inverse(Y3),Y3))) = inverse(X1),
inference(orient,[status(thm)],[t1264]) ).
cnf(t1241,plain,
inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),X2)),X3)))) = multiply(multiply(inverse(multiply(Y3,inverse(multiply(inverse(Y4),Y4)))),multiply(Y3,inverse(multiply(X1,inverse(X3))))),inverse(multiply(inverse(Y5),Y5))),
inference(cp,[status(thm)],[t478,t1137]) ).
cnf(t25561,plain,
inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),X2)),X3)))) = inverse(multiply(X1,inverse(X3))),
inference(step,[status(thm)],[t1241,t1072]) ).
cnf(t1300,plain,
inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),X2)),X3)))) = inverse(multiply(X1,inverse(X3))),
inference(orient,[status(thm)],[t25561]) ).
cnf(t639,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t572,t572]) ).
cnf(t640,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(X2),X2)),
inference(orient,[status(thm)],[t639]) ).
cnf(t1305,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),X2))),inverse(X2))) = inverse(multiply(inverse(X3),X3)),
inference(cp,[status(thm)],[t1300,t640]) ).
cnf(t1883,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),X2))),inverse(X2))) = inverse(multiply(inverse(X3),X3)),
inference(orient,[status(thm)],[t1305]) ).
cnf(t1929,plain,
inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),X2))) = multiply(multiply(inverse(multiply(X3,inverse(multiply(inverse(Y3),Y3)))),multiply(X3,inverse(inverse(X2)))),inverse(multiply(inverse(Y4),Y4))),
inference(cp,[status(thm)],[t478,t1883]) ).
cnf(t25566,plain,
inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),X2))) = inverse(inverse(X2)),
inference(step,[status(thm)],[t1929,t1072]) ).
cnf(t2085,plain,
inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),X2))) = inverse(inverse(X2)),
inference(orient,[status(thm)],[t25566]) ).
cnf(t2090,plain,
inverse(inverse(multiply(inverse(inverse(X1)),inverse(X2)))) = inverse(inverse(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(X2))))),
inference(cp,[status(thm)],[t2085,t233]) ).
cnf(t2139,plain,
inverse(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))))) = inverse(inverse(multiply(inverse(inverse(X2)),inverse(X3)))),
inference(orient,[status(thm)],[t2090]) ).
cnf(t4364,plain,
inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3)))) = multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X2)),inverse(X3)))),inverse(multiply(inverse(Y3),Y3)))),multiply(inverse(Y4),Y4)),inverse(multiply(inverse(Y5),Y5))),
inference(cp,[status(thm)],[t4339,t2139]) ).
cnf(t25574,plain,
inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3)))) = inverse(multiply(inverse(inverse(X2)),inverse(X3))),
inference(step,[status(thm)],[t4364,t4339]) ).
cnf(t5074,plain,
inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3)))) = inverse(multiply(inverse(inverse(X2)),inverse(X3))),
inference(orient,[status(thm)],[t25574]) ).
cnf(t1270,plain,
inverse(inverse(multiply(inverse(X1),X1))) = multiply(inverse(multiply(X2,inverse(multiply(multiply(inverse(X3),X3),Y3)))),multiply(X2,inverse(Y3))),
inference(cp,[status(thm)],[t1030,t1250]) ).
cnf(t3758,plain,
inverse(inverse(multiply(inverse(X1),X1))) = multiply(inverse(multiply(X2,inverse(multiply(multiply(inverse(X3),X3),Y3)))),multiply(X2,inverse(Y3))),
inference(orient,[status(thm)],[t1270]) ).
cnf(t4362,plain,
inverse(multiply(inverse(multiply(inverse(X1),X1)),X2)) = multiply(multiply(inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(X3),X3)))),multiply(inverse(Y3),Y3)),inverse(multiply(inverse(Y4),Y4))),
inference(cp,[status(thm)],[t4339,t2085]) ).
cnf(t25571,plain,
inverse(multiply(inverse(multiply(inverse(X1),X1)),X2)) = inverse(X2),
inference(step,[status(thm)],[t4362,t4339]) ).
cnf(t4738,plain,
inverse(multiply(inverse(multiply(inverse(X1),X1)),X2)) = inverse(X2),
inference(orient,[status(thm)],[t25571]) ).
cnf(t2088,plain,
inverse(inverse(multiply(inverse(inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X3))),inverse(X3)))) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t2085,t1030]) ).
cnf(t2323,plain,
inverse(inverse(multiply(inverse(inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X3))),inverse(X3)))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t2088]) ).
cnf(t4361,plain,
inverse(multiply(inverse(inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X3))),inverse(X3))) = multiply(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(Y3),Y3)))),multiply(inverse(Y4),Y4)),inverse(multiply(inverse(Y5),Y5))),
inference(cp,[status(thm)],[t4339,t2323]) ).
cnf(t25575,plain,
inverse(multiply(inverse(inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X3))),inverse(X3))) = inverse(X1),
inference(step,[status(thm)],[t4361,t4339]) ).
cnf(t5246,plain,
inverse(multiply(inverse(inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X3))),inverse(X3))) = inverse(X1),
inference(orient,[status(thm)],[t25575]) ).
cnf(t5249,plain,
inverse(inverse(inverse(multiply(inverse(X1),X1)))) = inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X3),X3))))),
inference(cp,[status(thm)],[t5246,t690]) ).
cnf(t14398,plain,
inverse(inverse(inverse(multiply(inverse(X1),X1)))) = inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X3),X3))))),
inference(orient,[status(thm)],[t5249]) ).
cnf(t14850,plain,
inverse(X1) = inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),X1)),
inference(cp,[status(thm)],[t4738,t14398]) ).
cnf(t14942,plain,
inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),X1)))),X2)) = inverse(X2),
inference(orient,[status(thm)],[t14850]) ).
cnf(t14949,plain,
inverse(inverse(inverse(multiply(inverse(X1),X1)))) = inverse(multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t14942,t640]) ).
cnf(t15181,plain,
inverse(inverse(inverse(multiply(inverse(X1),X1)))) = inverse(multiply(inverse(X2),X2)),
inference(orient,[status(thm)],[t14949]) ).
cnf(t15182,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(multiply(X2,inverse(multiply(multiply(inverse(X3),X3),Y3)))),multiply(X2,inverse(Y3)))),
inference(cp,[status(thm)],[t15181,t3758]) ).
cnf(t25588,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(inverse(multiply(multiply(inverse(X3),X3),Y3))),inverse(Y3))),
inference(step,[status(thm)],[t15182,t5074]) ).
cnf(t16586,plain,
inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(inverse(multiply(multiply(inverse(X2),X2),X3))),inverse(X3))),
inference(orient,[status(thm)],[t25588]) ).
cnf(t17057,plain,
inverse(inverse(multiply(multiply(inverse(X1),X1),X2))) = multiply(multiply(inverse(multiply(X3,inverse(multiply(inverse(Y3),Y3)))),multiply(X3,inverse(inverse(X2)))),inverse(multiply(inverse(Y4),Y4))),
inference(cp,[status(thm)],[t478,t16586]) ).
cnf(t25589,plain,
inverse(inverse(multiply(multiply(inverse(X1),X1),X2))) = inverse(inverse(X2)),
inference(step,[status(thm)],[t17057,t1072]) ).
cnf(t17132,plain,
inverse(inverse(multiply(multiply(inverse(X1),X1),X2))) = inverse(inverse(X2)),
inference(orient,[status(thm)],[t25589]) ).
cnf(t17251,plain,
multiply(inverse(X1),X1) = multiply(inverse(inverse(X2)),inverse(multiply(multiply(inverse(X3),X3),X2))),
inference(cp,[status(thm)],[t1250,t17132]) ).
cnf(t17326,plain,
multiply(inverse(X1),X1) = multiply(inverse(inverse(X2)),inverse(multiply(multiply(inverse(X3),X3),X2))),
inference(orient,[status(thm)],[t17251]) ).
cnf(t17638,plain,
inverse(inverse(multiply(inverse(X1),X1))) = multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(inverse(X3)),inverse(X3))),
inference(cp,[status(thm)],[t3758,t17326]) ).
cnf(t682,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(inverse(X2)),inverse(X3))),
inference(cp,[status(thm)],[t233,t640]) ).
cnf(t12885,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(inverse(Y3),Y3)),multiply(inverse(inverse(X2)),inverse(X3))),
inference(orient,[status(thm)],[t682]) ).
cnf(t25596,plain,
inverse(inverse(multiply(inverse(X1),X1))) = multiply(inverse(multiply(c3,inverse(X3))),multiply(c3,inverse(X3))),
inference(step,[status(thm)],[t17638,t12885]) ).
cnf(t4848,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(inverse(multiply(inverse(X3),X3)),X2)),
inference(cp,[status(thm)],[t1250,t4738]) ).
cnf(t4884,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(inverse(multiply(inverse(X3),X3)),X2)),
inference(orient,[status(thm)],[t4848]) ).
cnf(t25597,plain,
inverse(inverse(multiply(inverse(X1),X1))) = multiply(inverse(c3),multiply(inverse(multiply(inverse(c3),c3)),c3)),
inference(step,[status(thm)],[t25596,t4884]) ).
cnf(t25598,plain,
inverse(inverse(multiply(inverse(X1),X1))) = multiply(inverse(c3),c3),
inference(step,[status(thm)],[t25597,t4884]) ).
cnf(t20340,plain,
inverse(inverse(multiply(inverse(X1),X1))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t25598]) ).
cnf(t1374,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(multiply(inverse(multiply(inverse(Y3),Y3)),X3)))),
inference(cp,[status(thm)],[t1250,t1300]) ).
cnf(t2601,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(multiply(inverse(multiply(inverse(Y3),Y3)),X3)))),
inference(orient,[status(thm)],[t1374]) ).
cnf(t2702,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),multiply(X2,inverse(multiply(inverse(Y3),Y3)))),
inference(cp,[status(thm)],[t2601,t534]) ).
cnf(t2862,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),multiply(X2,inverse(multiply(inverse(Y3),Y3)))),
inference(orient,[status(thm)],[t2702]) ).
cnf(t20345,plain,
multiply(inverse(c3),c3) = inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(multiply(inverse(X3),X3)))))),
inference(cp,[status(thm)],[t20340,t2862]) ).
cnf(t25607,plain,
multiply(inverse(c3),c3) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X3),X3))))),
inference(step,[status(thm)],[t20345,t2139]) ).
cnf(t2170,plain,
inverse(inverse(multiply(inverse(inverse(X1)),inverse(X2)))) = inverse(inverse(multiply(inverse(multiply(inverse(inverse(X2)),inverse(X1))),multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t2139,t1250]) ).
cnf(t2401,plain,
inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X2))),multiply(inverse(X3),X3)))) = inverse(inverse(multiply(inverse(inverse(X2)),inverse(X1)))),
inference(orient,[status(thm)],[t2170]) ).
cnf(t4363,plain,
inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X2))),multiply(inverse(X3),X3))) = multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X2)),inverse(X1)))),inverse(multiply(inverse(Y3),Y3)))),multiply(inverse(Y4),Y4)),inverse(multiply(inverse(Y5),Y5))),
inference(cp,[status(thm)],[t4339,t2401]) ).
cnf(t25576,plain,
inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X2))),multiply(inverse(X3),X3))) = inverse(multiply(inverse(inverse(X2)),inverse(X1))),
inference(step,[status(thm)],[t4363,t4339]) ).
cnf(t5396,plain,
inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X2))),multiply(inverse(X3),X3))) = inverse(multiply(inverse(inverse(X2)),inverse(X1))),
inference(orient,[status(thm)],[t25576]) ).
cnf(t2330,plain,
inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))))) = inverse(inverse(multiply(inverse(inverse(multiply(X2,Y3))),inverse(Y3)))),
inference(cp,[status(thm)],[t2323,t478]) ).
cnf(t25568,plain,
inverse(inverse(multiply(inverse(inverse(multiply(X2,X3))),inverse(X3)))) = inverse(inverse(multiply(inverse(inverse(multiply(X2,Y3))),inverse(Y3)))),
inference(step,[status(thm)],[t2330,t2139]) ).
cnf(t2759,plain,
inverse(inverse(multiply(inverse(inverse(multiply(X1,X2))),inverse(X2)))) = inverse(inverse(multiply(inverse(inverse(multiply(X1,X3))),inverse(X3)))),
inference(orient,[status(thm)],[t25568]) ).
cnf(t4366,plain,
inverse(multiply(inverse(inverse(multiply(X1,X2))),inverse(X2))) = multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(X1,X3))),inverse(X3)))),inverse(multiply(inverse(Y3),Y3)))),multiply(inverse(Y4),Y4)),inverse(multiply(inverse(Y5),Y5))),
inference(cp,[status(thm)],[t4339,t2759]) ).
cnf(t25577,plain,
inverse(multiply(inverse(inverse(multiply(X1,X2))),inverse(X2))) = inverse(multiply(inverse(inverse(multiply(X1,X3))),inverse(X3))),
inference(step,[status(thm)],[t4366,t4339]) ).
cnf(t5673,plain,
inverse(multiply(inverse(inverse(multiply(X1,X2))),inverse(X2))) = inverse(multiply(inverse(inverse(multiply(X1,X3))),inverse(X3))),
inference(orient,[status(thm)],[t25577]) ).
cnf(t5735,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(multiply(inverse(multiply(inverse(inverse(multiply(X2,X3))),inverse(X3))),multiply(inverse(Y3),Y3))),
inference(cp,[status(thm)],[t5396,t5673]) ).
cnf(t25578,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(multiply(inverse(inverse(X3)),inverse(multiply(X2,X3)))),
inference(step,[status(thm)],[t5735,t5396]) ).
cnf(t5844,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(multiply(inverse(inverse(X3)),inverse(multiply(X2,X3)))),
inference(orient,[status(thm)],[t25578]) ).
cnf(t15333,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(multiply(inverse(multiply(inverse(X3),X3)),inverse(multiply(X2,inverse(multiply(inverse(Y3),Y3)))))),
inference(cp,[status(thm)],[t5844,t15181]) ).
cnf(t25595,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(inverse(multiply(X2,inverse(multiply(inverse(Y3),Y3))))),
inference(step,[status(thm)],[t15333,t4738]) ).
cnf(t19722,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(inverse(multiply(X2,inverse(multiply(inverse(X3),X3))))),
inference(orient,[status(thm)],[t25595]) ).
cnf(t25608,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(inverse(c3)),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),c3)))),
inference(step,[status(thm)],[t25607,t19722]) ).
cnf(t25609,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(inverse(c3)),inverse(multiply(multiply(inverse(c3),c3),c3)))),
inference(step,[status(thm)],[t25608,t20340]) ).
cnf(t25610,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(c3),c3)),
inference(step,[status(thm)],[t25609,t17326]) ).
cnf(t20517,plain,
inverse(multiply(inverse(c3),c3)) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t25610]) ).
cnf(t20518,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(X1),X1)),
inference(cp,[status(thm)],[t20517,t640]) ).
cnf(t20674,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t20518]) ).
cnf(t25626,plain,
multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),multiply(inverse(c3),c3)) = X2,
inference(step,[status(thm)],[t478,t20674]) ).
cnf(t20748,plain,
multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),multiply(inverse(c3),c3)) = X2,
inference(rw,[status(thm)],[t25626]) ).
cnf(t23304,plain,
multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),multiply(inverse(c3),c3)) = X2,
inference(orient,[status(thm)],[t20748]) ).
cnf(t25625,plain,
inverse(multiply(multiply(inverse(c3),c3),X2)) = inverse(X2),
inference(step,[status(thm)],[t4738,t20674]) ).
cnf(t20747,plain,
inverse(multiply(multiply(inverse(c3),c3),X2)) = inverse(X2),
inference(rw,[status(thm)],[t25625]) ).
cnf(t20762,plain,
inverse(multiply(multiply(inverse(c3),c3),X1)) = inverse(X1),
inference(orient,[status(thm)],[t20747]) ).
cnf(t20763,plain,
inverse(X1) = inverse(multiply(multiply(inverse(X2),X2),X1)),
inference(cp,[status(thm)],[t20762,t1250]) ).
cnf(t20800,plain,
inverse(multiply(multiply(inverse(X1),X1),X2)) = inverse(X2),
inference(orient,[status(thm)],[t20763]) ).
cnf(t25633,plain,
inverse(multiply(inverse(inverse(multiply(multiply(X1,multiply(inverse(c3),c3)),X3))),inverse(X3))) = inverse(X1),
inference(step,[status(thm)],[t5246,t20674]) ).
cnf(t20754,plain,
inverse(multiply(inverse(inverse(multiply(multiply(X1,multiply(inverse(c3),c3)),X3))),inverse(X3))) = inverse(X1),
inference(rw,[status(thm)],[t25633]) ).
cnf(t21576,plain,
inverse(multiply(inverse(inverse(multiply(multiply(X1,multiply(inverse(c3),c3)),X2))),inverse(X2))) = inverse(X1),
inference(orient,[status(thm)],[t20754]) ).
cnf(t21579,plain,
inverse(X1) = inverse(multiply(inverse(inverse(multiply(multiply(X1,multiply(inverse(X2),X2)),X3))),inverse(X3))),
inference(cp,[status(thm)],[t21576,t1250]) ).
cnf(t21736,plain,
inverse(multiply(inverse(inverse(multiply(multiply(X1,multiply(inverse(X2),X2)),X3))),inverse(X3))) = inverse(X1),
inference(orient,[status(thm)],[t21579]) ).
cnf(t25617,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(multiply(inverse(c3),c3),X2)),
inference(step,[status(thm)],[t4884,t20674]) ).
cnf(t20741,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(multiply(inverse(c3),c3),X2)),
inference(rw,[status(thm)],[t25617]) ).
cnf(t21208,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(multiply(inverse(c3),c3),X2)),
inference(orient,[status(thm)],[t20741]) ).
cnf(t21254,plain,
inverse(multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2))) = inverse(multiply(inverse(inverse(multiply(inverse(X3),multiply(multiply(inverse(c3),c3),X3)))),inverse(X1))),
inference(cp,[status(thm)],[t5673,t21208]) ).
cnf(t5899,plain,
inverse(multiply(inverse(inverse(multiply(X1,X2))),inverse(X3))) = inverse(multiply(inverse(multiply(inverse(inverse(Y3)),inverse(multiply(X1,Y3)))),multiply(inverse(inverse(X2)),inverse(X3)))),
inference(cp,[status(thm)],[t5074,t5844]) ).
cnf(t7831,plain,
inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))),multiply(inverse(inverse(X3)),inverse(Y3)))) = inverse(multiply(inverse(inverse(multiply(X2,X3))),inverse(Y3))),
inference(orient,[status(thm)],[t5899]) ).
cnf(t17185,plain,
inverse(multiply(inverse(inverse(multiply(X1,multiply(multiply(inverse(X2),X2),X3)))),inverse(Y3))) = inverse(multiply(inverse(multiply(inverse(inverse(Y4)),inverse(multiply(X1,Y4)))),multiply(inverse(inverse(X3)),inverse(Y3)))),
inference(cp,[status(thm)],[t7831,t17132]) ).
cnf(t25591,plain,
inverse(multiply(inverse(inverse(multiply(X1,multiply(multiply(inverse(X2),X2),X3)))),inverse(Y3))) = inverse(multiply(inverse(inverse(multiply(X1,X3))),inverse(Y3))),
inference(step,[status(thm)],[t17185,t7831]) ).
cnf(t17664,plain,
inverse(multiply(inverse(inverse(multiply(X1,multiply(multiply(inverse(X2),X2),X3)))),inverse(Y3))) = inverse(multiply(inverse(inverse(multiply(X1,X3))),inverse(Y3))),
inference(orient,[status(thm)],[t25591]) ).
cnf(t25644,plain,
inverse(multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2))) = inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(X1))),
inference(step,[status(thm)],[t21254,t17664]) ).
cnf(t25645,plain,
inverse(multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2))) = inverse(multiply(multiply(inverse(c3),c3),inverse(X1))),
inference(step,[status(thm)],[t25644,t20340]) ).
cnf(t25646,plain,
inverse(multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t25645,t20762]) ).
cnf(t21272,plain,
inverse(multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t25646]) ).
cnf(t21293,plain,
multiply(inverse(c3),c3) = inverse(multiply(inverse(inverse(X1)),multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2)))),
inference(cp,[status(thm)],[t20674,t21272]) ).
cnf(t21811,plain,
inverse(multiply(inverse(inverse(X1)),multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2)))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t21293]) ).
cnf(t21848,plain,
inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2))))),inverse(X3))) = inverse(multiply(inverse(multiply(Y3,multiply(inverse(c3),c3))),multiply(Y3,inverse(X3)))),
inference(cp,[status(thm)],[t5074,t21811]) ).
cnf(t25647,plain,
inverse(multiply(inverse(multiply(inverse(c3),c3)),inverse(X3))) = inverse(multiply(inverse(multiply(Y3,multiply(inverse(c3),c3))),multiply(Y3,inverse(X3)))),
inference(step,[status(thm)],[t21848,t21811]) ).
cnf(t25648,plain,
inverse(multiply(multiply(inverse(c3),c3),inverse(X3))) = inverse(multiply(inverse(multiply(Y3,multiply(inverse(c3),c3))),multiply(Y3,inverse(X3)))),
inference(step,[status(thm)],[t25647,t20517]) ).
cnf(t25649,plain,
inverse(inverse(X3)) = inverse(multiply(inverse(multiply(Y3,multiply(inverse(c3),c3))),multiply(Y3,inverse(X3)))),
inference(step,[status(thm)],[t25648,t20762]) ).
cnf(t21884,plain,
inverse(multiply(inverse(multiply(X1,multiply(inverse(c3),c3))),multiply(X1,inverse(X2)))) = inverse(inverse(X2)),
inference(orient,[status(thm)],[t25649]) ).
cnf(t21886,plain,
inverse(inverse(X1)) = inverse(multiply(inverse(multiply(X2,multiply(inverse(X3),X3))),multiply(X2,inverse(X1)))),
inference(cp,[status(thm)],[t21884,t1250]) ).
cnf(t21932,plain,
inverse(multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,inverse(X3)))) = inverse(inverse(X3)),
inference(orient,[status(thm)],[t21886]) ).
cnf(t20822,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(multiply(inverse(X3),X3),X2)),
inference(cp,[status(thm)],[t1250,t20800]) ).
cnf(t21390,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(multiply(inverse(X3),X3),X2)),
inference(orient,[status(thm)],[t20822]) ).
cnf(t21951,plain,
inverse(inverse(X1)) = inverse(multiply(inverse(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2))),multiply(inverse(X3),multiply(multiply(inverse(Y3),Y3),X3)))),
inference(cp,[status(thm)],[t21932,t21390]) ).
cnf(t7926,plain,
inverse(multiply(inverse(inverse(multiply(X1,multiply(inverse(multiply(inverse(X2),X2)),X3)))),inverse(Y3))) = inverse(multiply(inverse(multiply(inverse(inverse(Y4)),inverse(multiply(X1,Y4)))),multiply(inverse(inverse(X3)),inverse(Y3)))),
inference(cp,[status(thm)],[t7831,t4738]) ).
cnf(t25581,plain,
inverse(multiply(inverse(inverse(multiply(X1,multiply(inverse(multiply(inverse(X2),X2)),X3)))),inverse(Y3))) = inverse(multiply(inverse(inverse(multiply(X1,X3))),inverse(Y3))),
inference(step,[status(thm)],[t7926,t7831]) ).
cnf(t8096,plain,
inverse(multiply(inverse(inverse(multiply(X1,multiply(inverse(multiply(inverse(X2),X2)),X3)))),inverse(Y3))) = inverse(multiply(inverse(inverse(multiply(X1,X3))),inverse(Y3))),
inference(orient,[status(thm)],[t25581]) ).
cnf(t8225,plain,
inverse(multiply(X1,multiply(inverse(multiply(inverse(X2),X2)),X3))) = multiply(multiply(inverse(multiply(inverse(inverse(multiply(X1,X3))),inverse(multiply(inverse(Y3),Y3)))),multiply(inverse(Y4),Y4)),inverse(multiply(inverse(Y5),Y5))),
inference(cp,[status(thm)],[t4339,t8096]) ).
cnf(t25582,plain,
inverse(multiply(X1,multiply(inverse(multiply(inverse(X2),X2)),X3))) = inverse(multiply(X1,X3)),
inference(step,[status(thm)],[t8225,t4339]) ).
cnf(t8368,plain,
inverse(multiply(X1,multiply(inverse(multiply(inverse(X2),X2)),X3))) = inverse(multiply(X1,X3)),
inference(orient,[status(thm)],[t25582]) ).
cnf(t8423,plain,
inverse(multiply(inverse(inverse(multiply(X1,multiply(X2,multiply(inverse(multiply(inverse(X3),X3)),Y3))))),inverse(Y4))) = inverse(multiply(inverse(multiply(inverse(inverse(Y5)),inverse(multiply(X1,Y5)))),multiply(inverse(inverse(multiply(X2,Y3))),inverse(Y4)))),
inference(cp,[status(thm)],[t7831,t8368]) ).
cnf(t25583,plain,
inverse(multiply(inverse(inverse(multiply(X1,multiply(X2,multiply(inverse(multiply(inverse(X3),X3)),Y3))))),inverse(Y4))) = inverse(multiply(inverse(inverse(multiply(X1,multiply(X2,Y3)))),inverse(Y4))),
inference(step,[status(thm)],[t8423,t7831]) ).
cnf(t10611,plain,
inverse(multiply(inverse(inverse(multiply(X1,multiply(X2,multiply(inverse(multiply(inverse(X3),X3)),Y3))))),inverse(Y4))) = inverse(multiply(inverse(inverse(multiply(X1,multiply(X2,Y3)))),inverse(Y4))),
inference(orient,[status(thm)],[t25583]) ).
cnf(t10773,plain,
inverse(multiply(X1,multiply(X2,multiply(inverse(multiply(inverse(X3),X3)),Y3)))) = multiply(multiply(inverse(multiply(inverse(inverse(multiply(X1,multiply(X2,Y3)))),inverse(multiply(inverse(Y4),Y4)))),multiply(inverse(Y5),Y5)),inverse(multiply(inverse(Y6),Y6))),
inference(cp,[status(thm)],[t4339,t10611]) ).
cnf(t25584,plain,
inverse(multiply(X1,multiply(X2,multiply(inverse(multiply(inverse(X3),X3)),Y3)))) = inverse(multiply(X1,multiply(X2,Y3))),
inference(step,[status(thm)],[t10773,t4339]) ).
cnf(t10932,plain,
inverse(multiply(X1,multiply(X2,multiply(inverse(multiply(inverse(X3),X3)),Y3)))) = inverse(multiply(X1,multiply(X2,Y3))),
inference(orient,[status(thm)],[t25584]) ).
cnf(t25630,plain,
inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(c3),c3),Y3)))) = inverse(multiply(X1,multiply(X2,Y3))),
inference(step,[status(thm)],[t10932,t20674]) ).
cnf(t20751,plain,
inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(c3),c3),Y3)))) = inverse(multiply(X1,multiply(X2,Y3))),
inference(rw,[status(thm)],[t25630]) ).
cnf(t21472,plain,
inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(c3),c3),X3)))) = inverse(multiply(X1,multiply(X2,X3))),
inference(orient,[status(thm)],[t20751]) ).
cnf(t21483,plain,
inverse(multiply(X1,multiply(X2,X3))) = inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(Y3),Y3),X3)))),
inference(cp,[status(thm)],[t21472,t1250]) ).
cnf(t21517,plain,
inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X3),X3),Y3)))) = inverse(multiply(X1,multiply(X2,Y3))),
inference(orient,[status(thm)],[t21483]) ).
cnf(t25651,plain,
inverse(inverse(X1)) = inverse(multiply(inverse(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2))),multiply(inverse(X3),X3))),
inference(step,[status(thm)],[t21951,t21517]) ).
cnf(t22048,plain,
inverse(multiply(inverse(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2))),multiply(inverse(X3),X3))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t25651]) ).
cnf(t21601,plain,
inverse(inverse(inverse(multiply(multiply(X1,multiply(inverse(c3),c3)),X2)))) = inverse(multiply(inverse(inverse(X1)),inverse(inverse(X2)))),
inference(cp,[status(thm)],[t21272,t21576]) ).
cnf(t21633,plain,
inverse(inverse(inverse(multiply(multiply(X1,multiply(inverse(c3),c3)),X2)))) = inverse(multiply(inverse(inverse(X1)),inverse(inverse(X2)))),
inference(orient,[status(thm)],[t21601]) ).
cnf(t21636,plain,
inverse(multiply(inverse(inverse(X1)),inverse(inverse(X2)))) = inverse(inverse(inverse(multiply(multiply(X1,multiply(inverse(X3),X3)),X2)))),
inference(cp,[status(thm)],[t21633,t1250]) ).
cnf(t21675,plain,
inverse(inverse(inverse(multiply(multiply(X1,multiply(inverse(X2),X2)),X3)))) = inverse(multiply(inverse(inverse(X1)),inverse(inverse(X3)))),
inference(orient,[status(thm)],[t21636]) ).
cnf(t23367,plain,
inverse(multiply(inverse(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))))),inverse(inverse(multiply(inverse(c3),c3))))) = inverse(inverse(inverse(X2))),
inference(cp,[status(thm)],[t21675,t23304]) ).
cnf(t21303,plain,
inverse(inverse(inverse(multiply(inverse(X1),X2)))) = inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(X2)))),
inference(cp,[status(thm)],[t21272,t21272]) ).
cnf(t21335,plain,
inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(X2)))) = inverse(inverse(inverse(multiply(inverse(X1),X2)))),
inference(orient,[status(thm)],[t21303]) ).
cnf(t25658,plain,
inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))),multiply(inverse(c3),c3))))) = inverse(inverse(inverse(X2))),
inference(step,[status(thm)],[t23367,t21335]) ).
cnf(t23369,plain,
inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1))))) = inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(c3),c3)))),
inference(cp,[status(thm)],[t21736,t23304]) ).
cnf(t25620,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(inverse(multiply(X2,multiply(inverse(c3),c3)))),
inference(step,[status(thm)],[t19722,t20674]) ).
cnf(t20743,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(inverse(multiply(X2,multiply(inverse(c3),c3)))),
inference(rw,[status(thm)],[t25620]) ).
cnf(t20965,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(inverse(multiply(X2,multiply(inverse(c3),c3)))),
inference(orient,[status(thm)],[t20743]) ).
cnf(t25656,plain,
inverse(inverse(inverse(multiply(X2,multiply(inverse(c3),c3))))) = inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(c3),c3)))),
inference(step,[status(thm)],[t23369,t20965]) ).
cnf(t25657,plain,
inverse(inverse(inverse(multiply(X2,multiply(inverse(c3),c3))))) = inverse(multiply(inverse(inverse(X2)),multiply(inverse(c3),c3))),
inference(step,[status(thm)],[t25656,t20517]) ).
cnf(t23376,plain,
inverse(inverse(inverse(multiply(X1,multiply(inverse(c3),c3))))) = inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t25657]) ).
cnf(t25659,plain,
inverse(multiply(inverse(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))))),multiply(inverse(c3),c3))) = inverse(inverse(inverse(X2))),
inference(step,[status(thm)],[t25658,t23376]) ).
cnf(t21298,plain,
inverse(inverse(multiply(inverse(inverse(multiply(inverse(X1),X2))),multiply(inverse(c3),c3)))) = inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(X1)))),
inference(cp,[status(thm)],[t20965,t21272]) ).
cnf(t20972,plain,
inverse(inverse(multiply(inverse(X1),multiply(inverse(c3),c3)))) = inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3))),
inference(cp,[status(thm)],[t20965,t20674]) ).
cnf(t21019,plain,
inverse(inverse(multiply(inverse(X1),multiply(inverse(c3),c3)))) = inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t20972]) ).
cnf(t25654,plain,
inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),X2)))),multiply(inverse(c3),c3))) = inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(X1)))),
inference(step,[status(thm)],[t21298,t21019]) ).
cnf(t25655,plain,
inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),X2)))),multiply(inverse(c3),c3))) = inverse(inverse(inverse(multiply(inverse(X2),X1)))),
inference(step,[status(thm)],[t25654,t21335]) ).
cnf(t22245,plain,
inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),X2)))),multiply(inverse(c3),c3))) = inverse(inverse(inverse(multiply(inverse(X2),X1)))),
inference(orient,[status(thm)],[t25655]) ).
cnf(t25660,plain,
inverse(inverse(inverse(multiply(inverse(inverse(multiply(X2,X1))),inverse(X1))))) = inverse(inverse(inverse(X2))),
inference(step,[status(thm)],[t25659,t22245]) ).
cnf(t23527,plain,
inverse(inverse(inverse(multiply(inverse(inverse(multiply(X1,X2))),inverse(X2))))) = inverse(inverse(inverse(X1))),
inference(orient,[status(thm)],[t25660]) ).
cnf(t23528,plain,
inverse(inverse(inverse(multiply(X1,multiply(inverse(X2),X2))))) = inverse(inverse(inverse(X1))),
inference(cp,[status(thm)],[t23527,t21736]) ).
cnf(t23380,plain,
inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3))) = inverse(inverse(inverse(multiply(X1,multiply(inverse(X2),X2))))),
inference(cp,[status(thm)],[t23376,t1250]) ).
cnf(t23441,plain,
inverse(inverse(inverse(multiply(X1,multiply(inverse(X2),X2))))) = inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3))),
inference(orient,[status(thm)],[t23380]) ).
cnf(t25661,plain,
inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3))) = inverse(inverse(inverse(X1))),
inference(step,[status(thm)],[t23528,t23441]) ).
cnf(t23616,plain,
inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3))) = inverse(inverse(inverse(X1))),
inference(orient,[status(thm)],[t25661]) ).
cnf(t23627,plain,
inverse(inverse(inverse(X1))) = inverse(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t23616,t1250]) ).
cnf(t23918,plain,
inverse(multiply(inverse(inverse(X1)),multiply(inverse(X2),X2))) = inverse(inverse(inverse(X1))),
inference(orient,[status(thm)],[t23627]) ).
cnf(t25673,plain,
inverse(multiply(inverse(inverse(inverse(X1))),multiply(inverse(X3),X3))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t22048,t23918]) ).
cnf(t25674,plain,
inverse(inverse(inverse(inverse(X1)))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t25673,t23918]) ).
cnf(t23998,plain,
inverse(inverse(inverse(inverse(X1)))) = inverse(inverse(X1)),
inference(rw,[status(thm)],[t25674]) ).
cnf(t24000,plain,
inverse(inverse(inverse(inverse(X1)))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t23998]) ).
cnf(t25666,plain,
inverse(inverse(inverse(multiply(X1,multiply(inverse(X2),X2))))) = inverse(inverse(inverse(X1))),
inference(step,[status(thm)],[t23441,t23616]) ).
cnf(t23621,plain,
inverse(inverse(inverse(multiply(X1,multiply(inverse(X2),X2))))) = inverse(inverse(inverse(X1))),
inference(orient,[status(thm)],[t25666]) ).
cnf(t24003,plain,
inverse(inverse(multiply(X1,multiply(inverse(X2),X2)))) = inverse(inverse(inverse(inverse(X1)))),
inference(cp,[status(thm)],[t24000,t23621]) ).
cnf(t25676,plain,
inverse(inverse(multiply(X1,multiply(inverse(X2),X2)))) = inverse(inverse(X1)),
inference(step,[status(thm)],[t24003,t24000]) ).
cnf(t24068,plain,
inverse(inverse(multiply(X1,multiply(inverse(X2),X2)))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t25676]) ).
cnf(t24120,plain,
inverse(X1) = inverse(multiply(inverse(inverse(multiply(X1,multiply(inverse(X2),X2)))),inverse(multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t21736,t24068]) ).
cnf(t25679,plain,
inverse(X1) = inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X3),X3)))),
inference(step,[status(thm)],[t24120,t24068]) ).
cnf(t25680,plain,
inverse(X1) = inverse(multiply(inverse(inverse(X1)),multiply(inverse(c3),c3))),
inference(step,[status(thm)],[t25679,t20674]) ).
cnf(t25681,plain,
inverse(X1) = inverse(inverse(inverse(X1))),
inference(step,[status(thm)],[t25680,t23616]) ).
cnf(t24158,plain,
inverse(inverse(inverse(X1))) = inverse(X1),
inference(orient,[status(thm)],[t25681]) ).
cnf(t24170,plain,
inverse(X1) = inverse(multiply(multiply(inverse(X2),inverse(inverse(X2))),X1)),
inference(cp,[status(thm)],[t20800,t24158]) ).
cnf(t24499,plain,
inverse(multiply(multiply(inverse(X1),inverse(inverse(X1))),X2)) = inverse(X2),
inference(orient,[status(thm)],[t24170]) ).
cnf(t24520,plain,
multiply(inverse(X1),inverse(inverse(X1))) = multiply(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3))),multiply(inverse(c3),c3)),
inference(cp,[status(thm)],[t23304,t24499]) ).
cnf(t25611,plain,
multiply(inverse(c3),c3) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),X3))),
inference(step,[status(thm)],[t690,t20674]) ).
cnf(t25612,plain,
multiply(inverse(c3),c3) = multiply(multiply(inverse(X2),X2),multiply(inverse(c3),c3)),
inference(step,[status(thm)],[t25611,t20674]) ).
cnf(t20736,plain,
multiply(inverse(c3),c3) = multiply(multiply(inverse(X2),X2),multiply(inverse(c3),c3)),
inference(rw,[status(thm)],[t25612]) ).
cnf(t20844,plain,
multiply(multiply(inverse(X1),X1),multiply(inverse(c3),c3)) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t20736]) ).
cnf(t25694,plain,
multiply(inverse(X1),inverse(inverse(X1))) = multiply(inverse(c3),c3),
inference(step,[status(thm)],[t24520,t20844]) ).
cnf(t24560,plain,
multiply(inverse(X1),inverse(inverse(X1))) = multiply(inverse(c3),c3),
inference(orient,[status(thm)],[t25694]) ).
cnf(t24571,plain,
inverse(multiply(inverse(inverse(X1)),inverse(inverse(X2)))) = inverse(multiply(inverse(multiply(inverse(X2),inverse(X1))),multiply(inverse(c3),c3))),
inference(cp,[status(thm)],[t5074,t24560]) ).
cnf(t25686,plain,
inverse(multiply(inverse(X1),inverse(inverse(X2)))) = inverse(inverse(inverse(multiply(inverse(X1),X2)))),
inference(step,[status(thm)],[t21335,t24158]) ).
cnf(t25687,plain,
inverse(multiply(inverse(X1),inverse(inverse(X2)))) = inverse(multiply(inverse(X1),X2)),
inference(step,[status(thm)],[t25686,t24158]) ).
cnf(t24219,plain,
inverse(multiply(inverse(X1),inverse(inverse(X2)))) = inverse(multiply(inverse(X1),X2)),
inference(rw,[status(thm)],[t25687]) ).
cnf(t24355,plain,
inverse(multiply(inverse(X1),inverse(inverse(X2)))) = inverse(multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t24219]) ).
cnf(t25695,plain,
inverse(multiply(inverse(inverse(X1)),X2)) = inverse(multiply(inverse(multiply(inverse(X2),inverse(X1))),multiply(inverse(c3),c3))),
inference(step,[status(thm)],[t24571,t24355]) ).
cnf(t24163,plain,
inverse(multiply(X1,multiply(inverse(X2),X2))) = inverse(inverse(inverse(X1))),
inference(cp,[status(thm)],[t24158,t24068]) ).
cnf(t25691,plain,
inverse(multiply(X1,multiply(inverse(X2),X2))) = inverse(X1),
inference(step,[status(thm)],[t24163,t24158]) ).
cnf(t24222,plain,
inverse(multiply(X1,multiply(inverse(X2),X2))) = inverse(X1),
inference(orient,[status(thm)],[t25691]) ).
cnf(t25696,plain,
inverse(multiply(inverse(inverse(X1)),X2)) = inverse(inverse(multiply(inverse(X2),inverse(X1)))),
inference(step,[status(thm)],[t25695,t24222]) ).
cnf(t24589,plain,
inverse(inverse(multiply(inverse(X1),inverse(X2)))) = inverse(multiply(inverse(inverse(X2)),X1)),
inference(orient,[status(thm)],[t25696]) ).
cnf(t24590,plain,
inverse(multiply(inverse(inverse(inverse(X1))),X2)) = inverse(inverse(multiply(inverse(X2),X1))),
inference(cp,[status(thm)],[t24589,t24355]) ).
cnf(t25697,plain,
inverse(multiply(inverse(X1),X2)) = inverse(inverse(multiply(inverse(X2),X1))),
inference(step,[status(thm)],[t24590,t24158]) ).
cnf(t24670,plain,
inverse(inverse(multiply(inverse(X1),X2))) = inverse(multiply(inverse(X2),X1)),
inference(orient,[status(thm)],[t25697]) ).
cnf(t25693,plain,
inverse(multiply(inverse(X1),multiply(X1,inverse(X3)))) = inverse(inverse(X3)),
inference(step,[status(thm)],[t21932,t24222]) ).
cnf(t24290,plain,
inverse(multiply(inverse(X1),multiply(X1,inverse(X3)))) = inverse(inverse(X3)),
inference(rw,[status(thm)],[t25693]) ).
cnf(t24427,plain,
inverse(multiply(inverse(X1),multiply(X1,inverse(X2)))) = inverse(inverse(X2)),
inference(orient,[status(thm)],[t24290]) ).
cnf(t24671,plain,
inverse(multiply(inverse(multiply(X1,inverse(X2))),X1)) = inverse(inverse(inverse(X2))),
inference(cp,[status(thm)],[t24670,t24427]) ).
cnf(t25701,plain,
inverse(multiply(inverse(multiply(X1,inverse(X2))),X1)) = inverse(X2),
inference(step,[status(thm)],[t24671,t24158]) ).
cnf(t24731,plain,
inverse(multiply(inverse(multiply(X1,inverse(X2))),X1)) = inverse(X2),
inference(orient,[status(thm)],[t25701]) ).
cnf(t25677,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(inverse(X2)),
inference(step,[status(thm)],[t20965,t24068]) ).
cnf(t24069,plain,
inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1)))) = inverse(inverse(X2)),
inference(orient,[status(thm)],[t25677]) ).
cnf(t24738,plain,
inverse(multiply(X1,X2)) = inverse(multiply(inverse(inverse(X1)),inverse(inverse(X2)))),
inference(cp,[status(thm)],[t24731,t24069]) ).
cnf(t25702,plain,
inverse(multiply(X1,X2)) = inverse(multiply(inverse(inverse(X1)),X2)),
inference(step,[status(thm)],[t24738,t24355]) ).
cnf(t24795,plain,
inverse(multiply(inverse(inverse(X1)),X2)) = inverse(multiply(X1,X2)),
inference(orient,[status(thm)],[t25702]) ).
cnf(t25703,plain,
inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3)))) = inverse(multiply(X2,inverse(X3))),
inference(step,[status(thm)],[t5074,t24795]) ).
cnf(t24796,plain,
inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3)))) = inverse(multiply(X2,inverse(X3))),
inference(orient,[status(thm)],[t25703]) ).
cnf(t24840,plain,
inverse(inverse(X1)) = multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),multiply(inverse(c3),c3)),
inference(cp,[status(thm)],[t23304,t24795]) ).
cnf(t25711,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t24840,t23304]) ).
cnf(t24865,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t25711]) ).
cnf(t25719,plain,
multiply(inverse(X1),X2) = inverse(multiply(inverse(X2),X1)),
inference(step,[status(thm)],[t24670,t24865]) ).
cnf(t24913,plain,
multiply(inverse(X1),X2) = inverse(multiply(inverse(X2),X1)),
inference(rw,[status(thm)],[t25719]) ).
cnf(t25002,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t24913]) ).
cnf(t25731,plain,
multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(X2))) = inverse(multiply(X2,inverse(X3))),
inference(step,[status(thm)],[t24796,t25002]) ).
cnf(t25028,plain,
multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(X2))) = inverse(multiply(X2,inverse(X3))),
inference(rw,[status(thm)],[t25731]) ).
cnf(t25007,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t25002,t24865]) ).
cnf(t25030,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t25007]) ).
cnf(t25033,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t25030,t24865]) ).
cnf(t25045,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t25033]) ).
cnf(t25744,plain,
multiply(multiply(X3,inverse(X1)),multiply(X1,inverse(X2))) = inverse(multiply(X2,inverse(X3))),
inference(step,[status(thm)],[t25028,t25045]) ).
cnf(t25745,plain,
multiply(multiply(X3,inverse(X1)),multiply(X1,inverse(X2))) = multiply(X3,inverse(X2)),
inference(step,[status(thm)],[t25744,t25045]) ).
cnf(t25473,plain,
multiply(multiply(X1,inverse(X2)),multiply(X2,inverse(X3))) = multiply(X1,inverse(X3)),
inference(orient,[status(thm)],[t25745]) ).
cnf(t25716,plain,
inverse(multiply(inverse(X1),multiply(X1,inverse(X2)))) = X2,
inference(step,[status(thm)],[t24427,t24865]) ).
cnf(t24870,plain,
inverse(multiply(inverse(X1),multiply(X1,inverse(X2)))) = X2,
inference(orient,[status(thm)],[t25716]) ).
cnf(t25730,plain,
multiply(inverse(multiply(X1,inverse(X2))),X1) = X2,
inference(step,[status(thm)],[t24870,t25002]) ).
cnf(t25027,plain,
multiply(inverse(multiply(X1,inverse(X2))),X1) = X2,
inference(rw,[status(thm)],[t25730]) ).
cnf(t25738,plain,
multiply(multiply(X2,inverse(X1)),X1) = X2,
inference(step,[status(thm)],[t25027,t25045]) ).
cnf(t25061,plain,
multiply(multiply(X1,inverse(X2)),X2) = X1,
inference(orient,[status(thm)],[t25738]) ).
cnf(t25067,plain,
X1 = multiply(multiply(X1,X2),inverse(X2)),
inference(cp,[status(thm)],[t25061,t24865]) ).
cnf(t25069,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(orient,[status(thm)],[t25067]) ).
cnf(t25475,plain,
multiply(multiply(X1,X2),inverse(X3)) = multiply(X1,multiply(X2,inverse(X3))),
inference(cp,[status(thm)],[t25473,t25069]) ).
cnf(t25504,plain,
multiply(multiply(X1,X2),inverse(X3)) = multiply(X1,multiply(X2,inverse(X3))),
inference(orient,[status(thm)],[t25475]) ).
cnf(t25523,plain,
multiply(X1,multiply(X2,inverse(inverse(X3)))) = multiply(multiply(X1,X2),X3),
inference(cp,[status(thm)],[t25504,t24865]) ).
cnf(t25752,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X2),X3),
inference(step,[status(thm)],[t25523,t24865]) ).
cnf(t25537,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t25752]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t25537]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP411-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n008.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Wed Sep 23 14:42:14 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 14.26/7.73 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.26/7.73 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------