%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : GRP419-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sat Jul 16 11:38:27 EDT 2022
% Result : Unsatisfiable 10.69s 10.92s
% Output : Refutation 10.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 2
% Syntax : Number of clauses : 135 ( 135 unt; 0 nHn; 4 RR)
% Number of literals : 135 ( 134 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 520 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(single_axiom,axiom,
inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z))) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
cnf(prove_these_axioms_2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_2) ).
cnf(3,plain,
inverse(multiply(inverse(multiply(X,inverse(multiply(Y,inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z))) = multiply(inverse(multiply(U,inverse(multiply(inverse(Y),inverse(multiply(V,inverse(multiply(inverse(V),V)))))))),multiply(U,V)),
inference('PARAMODULATE',[status(thm)],[single_axiom,single_axiom,theory(equality)]) ).
cnf(5,plain,
multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z)) = Y,
inference('PARAMODULATE',[status(thm)],[single_axiom,3,theory(equality)]) ).
cnf(6,plain,
inverse(inverse(multiply(inverse(multiply(X,inverse(multiply(Y,inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),multiply(X,Z)))) = Y,
inference('PARAMODULATE',[status(thm)],[single_axiom,3,theory(equality)]) ).
cnf(19,plain,
multiply(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),inverse(multiply(inverse(inverse(U)),inverse(multiply(multiply(X,Z),inverse(multiply(inverse(multiply(X,Z)),multiply(X,Z))))))))),Y) = U,
inference('PARAMODULATE',[status(thm)],[5,5,theory(equality)]) ).
cnf(20,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(inverse(Y)),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))))),inverse(multiply(inverse(U),inverse(multiply(multiply(X,Z),inverse(multiply(inverse(multiply(X,Z)),multiply(X,Z))))))))),Y)) = U,
inference('PARAMODULATE',[status(thm)],[single_axiom,5,theory(equality)]) ).
cnf(90,plain,
inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))) = multiply(inverse(multiply(U,inverse(multiply(inverse(inverse(inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))),inverse(multiply(V,inverse(multiply(inverse(V),V)))))))),inverse(multiply(inverse(Y),inverse(multiply(multiply(U,V),inverse(multiply(inverse(multiply(U,V)),multiply(U,V)))))))),
inference('PARAMODULATE',[status(thm)],[single_axiom,20,theory(equality)]) ).
cnf(163,plain,
inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))) = inverse(multiply(inverse(multiply(U,Y)),multiply(U,Z))),
inference('PARAMODULATE',[status(thm)],[90,90,theory(equality)]) ).
cnf(164,plain,
multiply(inverse(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,Z)))),inverse(multiply(Z,inverse(multiply(inverse(Z),Z))))) = Y,
inference('PARAMODULATE',[status(thm)],[19,90,theory(equality)]) ).
cnf(165,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z)))),inverse(multiply(Z,inverse(multiply(inverse(Z),Z)))))) = Y,
inference('PARAMODULATE',[status(thm)],[20,90,theory(equality)]) ).
cnf(265,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),V))) = inverse(multiply(inverse(multiply(W,multiply(U,Z))),multiply(W,V))),
inference('PARAMODULATE',[status(thm)],[163,163,theory(equality)]) ).
cnf(270,plain,
multiply(inverse(multiply(X,Y)),multiply(X,Z)) = multiply(inverse(multiply(U,Y)),multiply(U,Z)),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[5,163,theory(equality)]),5,theory(equality)]) ).
cnf(292,plain,
multiply(inverse(multiply(inverse(multiply(X,Y)),Z)),multiply(inverse(multiply(U,Y)),multiply(U,V))) = multiply(inverse(multiply(W,Z)),multiply(W,multiply(X,V))),
inference('PARAMODULATE',[status(thm)],[270,270,theory(equality)]) ).
cnf(293,plain,
multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),V)) = multiply(inverse(multiply(W,multiply(U,Z))),multiply(W,V)),
inference('PARAMODULATE',[status(thm)],[270,270,theory(equality)]) ).
cnf(294,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),Z)),multiply(inverse(multiply(U,Y)),multiply(U,V)))) = inverse(multiply(inverse(multiply(W,Z)),multiply(W,multiply(X,V)))),
inference('PARAMODULATE',[status(thm)],[163,270,theory(equality)]) ).
cnf(309,plain,
multiply(inverse(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,multiply(Z,U))))),inverse(multiply(multiply(Z,U),inverse(multiply(inverse(multiply(V,U)),multiply(V,U)))))) = Y,
inference('PARAMODULATE',[status(thm)],[164,163,theory(equality)]) ).
cnf(330,plain,
inverse(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z)))) = inverse(inverse(multiply(inverse(multiply(U,Y)),multiply(U,Z)))),
inference('PARAMODULATE',[status(thm)],[6,165,theory(equality)]) ).
cnf(335,plain,
multiply(inverse(inverse(multiply(X,multiply(inverse(inverse(multiply(inverse(multiply(Y,X)),multiply(Y,Z)))),U)))),inverse(multiply(U,inverse(multiply(inverse(U),U))))) = multiply(Z,inverse(multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[164,165,theory(equality)]) ).
cnf(464,plain,
multiply(inverse(multiply(X,multiply(Y,Z))),multiply(X,multiply(Y,U))) = multiply(inverse(multiply(V,multiply(W,Z))),multiply(V,multiply(W,U))),
inference('PARAMODULATE',[status(thm)],[292,293,theory(equality)]) ).
cnf(572,plain,
inverse(multiply(inverse(multiply(X,multiply(Y,Z))),multiply(X,multiply(Y,U)))) = inverse(multiply(inverse(multiply(V,multiply(W,Z))),multiply(V,multiply(W,U)))),
inference('PARAMODULATE',[status(thm)],[163,464,theory(equality)]) ).
cnf(589,plain,
multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,multiply(Z,U)))),multiply(inverse(multiply(inverse(multiply(Z,V)),Y)),multiply(inverse(multiply(W,V)),X1))) = multiply(inverse(multiply(Y1,multiply(Z1,multiply(W,U)))),multiply(Y1,multiply(Z1,X1))),
inference('PARAMODULATE',[status(thm)],[464,292,theory(equality)]) ).
cnf(844,plain,
multiply(multiply(X,Y),inverse(multiply(inverse(multiply(X,Y)),multiply(X,Y)))) = multiply(multiply(X,Y),inverse(multiply(inverse(multiply(Z,Y)),multiply(Z,Y)))),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[164,309,theory(equality)]),335,theory(equality)]) ).
cnf(905,plain,
multiply(X,inverse(multiply(inverse(X),X))) = multiply(X,inverse(multiply(inverse(multiply(Y,multiply(Z,U))),multiply(Y,multiply(Z,U))))),
inference('PARAMODULATE',[status(thm)],[844,5,theory(equality)]) ).
cnf(907,plain,
multiply(X,inverse(multiply(inverse(X),X))) = multiply(X,inverse(multiply(inverse(Y),Y))),
inference('PARAMODULATE',[status(thm)],[905,5,theory(equality)]) ).
cnf(908,plain,
multiply(X,inverse(multiply(inverse(Y),Y))) = multiply(X,inverse(multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[907,907,theory(equality)]) ).
cnf(909,plain,
multiply(inverse(multiply(X,inverse(multiply(inverse(Y),Y)))),multiply(X,Z)) = multiply(Z,inverse(multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[5,908,theory(equality)]) ).
cnf(910,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z)))),inverse(multiply(Z,inverse(multiply(inverse(U),U)))))) = Y,
inference('PARAMODULATE',[status(thm)],[165,908,theory(equality)]) ).
cnf(911,plain,
multiply(inverse(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,Z)))),inverse(multiply(Z,inverse(multiply(inverse(U),U))))) = Y,
inference('PARAMODULATE',[status(thm)],[164,908,theory(equality)]) ).
cnf(950,plain,
multiply(inverse(multiply(X,inverse(multiply(inverse(Y),Y)))),multiply(X,Z)) = multiply(Z,inverse(multiply(inverse(U),U))),
inference('PARAMODULATE',[status(thm)],[908,909,theory(equality)]) ).
cnf(1066,plain,
inverse(multiply(inverse(X),X)) = inverse(multiply(inverse(Y),Y)),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[910,908,theory(equality)]),911,theory(equality)]) ).
cnf(1072,plain,
inverse(multiply(inverse(multiply(X,inverse(multiply(inverse(Y),Y)))),multiply(X,inverse(inverse(multiply(inverse(multiply(Z,U)),multiply(Z,inverse(inverse(multiply(inverse(V),V)))))))))) = U,
inference('PARAMODULATE',[status(thm)],[910,950,theory(equality)]) ).
cnf(1110,plain,
inverse(inverse(multiply(inverse(X),X))) = inverse(inverse(multiply(inverse(multiply(Y,Z)),multiply(Y,Z)))),
inference('PARAMODULATE',[status(thm)],[330,1066,theory(equality)]) ).
cnf(1111,plain,
inverse(multiply(inverse(X),X)) = inverse(multiply(inverse(multiply(inverse(Y),Y)),multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[1066,1066,theory(equality)]) ).
cnf(1112,plain,
multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Z)) = multiply(inverse(multiply(U,Y)),multiply(U,Z)),
inference('PARAMODULATE',[status(thm)],[270,1066,theory(equality)]) ).
cnf(1116,plain,
inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Z))) = inverse(multiply(inverse(multiply(U,Y)),multiply(U,Z))),
inference('PARAMODULATE',[status(thm)],[163,1066,theory(equality)]) ).
cnf(1123,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Z)))),inverse(multiply(Z,inverse(multiply(inverse(U),U)))))) = Y,
inference('PARAMODULATE',[status(thm)],[910,1066,theory(equality)]) ).
cnf(1147,plain,
inverse(inverse(multiply(inverse(X),X))) = inverse(inverse(multiply(inverse(Y),Y))),
inference('PARAMODULATE',[status(thm)],[1110,1110,theory(equality)]) ).
cnf(1198,plain,
multiply(inverse(X),X) = multiply(inverse(Y),Y),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[910,1111,theory(equality)]),1123,theory(equality)]) ).
cnf(1253,plain,
multiply(multiply(inverse(X),X),a2) != a2,
inference('PARAMODULATE',[status(thm)],[prove_these_axioms_2,1198,theory(equality)]) ).
cnf(1254,plain,
multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Y)) = multiply(inverse(Z),Z),
inference('PARAMODULATE',[status(thm)],[1198,1066,theory(equality)]) ).
cnf(1255,plain,
multiply(inverse(X),X) = multiply(inverse(multiply(inverse(Y),Y)),inverse(multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[950,1198,theory(equality)]) ).
cnf(1256,plain,
multiply(inverse(X),X) = multiply(inverse(inverse(multiply(inverse(Y),Y))),inverse(multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[908,1198,theory(equality)]) ).
cnf(1257,plain,
multiply(inverse(multiply(inverse(X),Y)),multiply(inverse(Z),Z)) = multiply(inverse(multiply(U,Y)),multiply(U,X)),
inference('PARAMODULATE',[status(thm)],[270,1198,theory(equality)]) ).
cnf(1275,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(U),U))) = inverse(multiply(inverse(multiply(V,multiply(W,Z))),multiply(V,multiply(W,Y)))),
inference('PARAMODULATE',[status(thm)],[265,1198,theory(equality)]) ).
cnf(1277,plain,
inverse(multiply(inverse(multiply(X,multiply(inverse(Y),Z))),multiply(X,multiply(inverse(U),U)))) = inverse(multiply(inverse(multiply(V,multiply(W,Z))),multiply(V,multiply(W,Y)))),
inference('PARAMODULATE',[status(thm)],[572,1198,theory(equality)]) ).
cnf(1370,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),multiply(inverse(V),V)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(W),W)),multiply(U,Z))),multiply(inverse(X1),X1))),
inference('PARAMODULATE',[status(thm)],[265,1254,theory(equality)]) ).
cnf(1442,plain,
multiply(inverse(X),X) = inverse(multiply(inverse(Y),Y)),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[910,1255,theory(equality)]),1123,theory(equality)]) ).
cnf(1489,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),inverse(multiply(inverse(V),V))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(W),W)),multiply(U,Z))),multiply(inverse(X1),X1))),
inference('PARAMODULATE',[status(thm)],[265,1255,theory(equality)]) ).
cnf(1519,plain,
multiply(inverse(multiply(inverse(X),X)),a2) != a2,
inference('PARAMODULATE',[status(thm)],[1253,1442,theory(equality)]) ).
cnf(1520,plain,
multiply(inverse(X),X) = inverse(inverse(multiply(inverse(Y),Y))),
inference('PARAMODULATE',[status(thm)],[1442,1442,theory(equality)]) ).
cnf(1524,plain,
multiply(X,inverse(multiply(inverse(Y),Y))) = multiply(X,multiply(inverse(Z),Z)),
inference('PARAMODULATE',[status(thm)],[908,1442,theory(equality)]) ).
cnf(1527,plain,
multiply(inverse(X),X) = multiply(multiply(inverse(Y),Y),inverse(multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[1255,1442,theory(equality)]) ).
cnf(1533,plain,
multiply(inverse(inverse(multiply(inverse(X),X))),multiply(inverse(Y),Y)) = multiply(inverse(Z),Z),
inference('PARAMODULATE',[status(thm)],[1254,1442,theory(equality)]) ).
cnf(1536,plain,
multiply(inverse(X),X) = multiply(inverse(multiply(inverse(Y),Y)),inverse(inverse(multiply(inverse(Z),Z)))),
inference('PARAMODULATE',[status(thm)],[1255,1442,theory(equality)]) ).
cnf(1670,plain,
multiply(multiply(inverse(X),X),inverse(multiply(inverse(Y),Y))) = inverse(multiply(inverse(Z),Z)),
inference('PARAMODULATE',[status(thm)],[1442,1520,theory(equality)]) ).
cnf(1671,plain,
multiply(multiply(inverse(X),X),multiply(inverse(Y),Y)) = inverse(inverse(multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[1520,1442,theory(equality)]) ).
cnf(1672,plain,
multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Y)) = inverse(inverse(multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[1254,1520,theory(equality)]) ).
cnf(1673,plain,
inverse(inverse(multiply(inverse(X),X))) = inverse(inverse(inverse(inverse(multiply(inverse(Y),Y))))),
inference('PARAMODULATE',[status(thm)],[1147,1520,theory(equality)]) ).
cnf(1674,plain,
multiply(inverse(X),X) = inverse(multiply(multiply(inverse(Y),Y),inverse(multiply(inverse(Z),Z)))),
inference('PARAMODULATE',[status(thm)],[1442,1520,theory(equality)]) ).
cnf(1675,plain,
multiply(multiply(inverse(X),X),inverse(multiply(inverse(Y),Y))) = inverse(inverse(multiply(inverse(Z),Z))),
inference('PARAMODULATE',[status(thm)],[1520,1520,theory(equality)]) ).
cnf(2053,plain,
multiply(X,multiply(inverse(Y),Y)) = multiply(X,multiply(inverse(Z),Z)),
inference('PARAMODULATE',[status(thm)],[1524,1524,theory(equality)]) ).
cnf(2484,plain,
multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),Z)) = multiply(inverse(multiply(inverse(U),U)),multiply(inverse(Y),Z)),
inference('PARAMODULATE',[status(thm)],[1112,1112,theory(equality)]) ).
cnf(3089,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),inverse(multiply(inverse(V),V))))) = inverse(multiply(inverse(multiply(multiply(inverse(W),W),multiply(U,Z))),multiply(inverse(X1),X1))),
inference('PARAMODULATE',[status(thm)],[265,1527,theory(equality)]) ).
cnf(3624,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),inverse(multiply(inverse(V),V))))) = inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(W),W))),multiply(U,Z))),multiply(inverse(X1),X1))),
inference('PARAMODULATE',[status(thm)],[265,1256,theory(equality)]) ).
cnf(4775,plain,
multiply(inverse(multiply(inverse(X),Y)),multiply(inverse(Z),Z)) = multiply(inverse(inverse(multiply(inverse(U),U))),multiply(inverse(Y),X)),
inference('PARAMODULATE',[status(thm)],[1257,1442,theory(equality)]) ).
cnf(4973,plain,
multiply(inverse(multiply(inverse(X),Y)),multiply(inverse(multiply(inverse(multiply(Z,U)),multiply(Z,multiply(V,W)))),multiply(inverse(multiply(inverse(multiply(V,X1)),U)),multiply(inverse(multiply(Y1,X1)),multiply(Y1,W))))) = multiply(inverse(multiply(Z1,Y)),multiply(Z1,X)),
inference('PARAMODULATE',[status(thm)],[1257,294,theory(equality)]) ).
cnf(5505,plain,
multiply(inverse(multiply(X,multiply(Y,Z))),multiply(X,multiply(Y,U))) = multiply(inverse(multiply(inverse(inverse(multiply(inverse(V),V))),multiply(inverse(U),Z))),multiply(inverse(W),W)),
inference('PARAMODULATE',[status(thm)],[464,1533,theory(equality)]) ).
cnf(6181,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(X,Y)),multiply(X,multiply(inverse(Z),Z))))),inverse(inverse(multiply(inverse(U),U))))) = Y,
inference('PARAMODULATE',[status(thm)],[910,1670,theory(equality)]) ).
cnf(7111,plain,
inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),multiply(inverse(Z),Z)))) = inverse(multiply(inverse(multiply(U,Y)),multiply(U,multiply(inverse(V),V)))),
inference('PARAMODULATE',[status(thm)],[1116,2053,theory(equality)]) ).
cnf(7149,plain,
inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(multiply(Y,Z)),multiply(Y,U)))) = inverse(multiply(inverse(multiply(V,multiply(inverse(U),Z))),multiply(V,multiply(inverse(W),W)))),
inference('PARAMODULATE',[status(thm)],[1116,1257,theory(equality)]) ).
cnf(7292,plain,
inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(multiply(Y,inverse(multiply(inverse(Z),Z)))),multiply(Y,inverse(U))))) = inverse(multiply(inverse(multiply(V,U)),multiply(V,inverse(multiply(inverse(W),W))))),
inference('PARAMODULATE',[status(thm)],[1116,950,theory(equality)]) ).
cnf(7303,plain,
inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),multiply(inverse(Z),Z)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(U),V)),Y)),multiply(inverse(multiply(W,V)),multiply(W,U)))),
inference('PARAMODULATE',[status(thm)],[1116,1257,theory(equality)]) ).
cnf(7597,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(U),U))) = inverse(multiply(inverse(multiply(V,multiply(inverse(Y),Z))),multiply(V,inverse(inverse(multiply(inverse(W),W)))))),
inference('PARAMODULATE',[status(thm)],[265,1536,theory(equality)]) ).
cnf(8365,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(X),Y)),Z)),multiply(inverse(multiply(U,Y)),multiply(U,X)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(V),V)),Z)),inverse(inverse(multiply(inverse(W),W))))),
inference('PARAMODULATE',[status(thm)],[294,1672,theory(equality)]) ).
cnf(8366,plain,
inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X),X)),Y)),inverse(inverse(multiply(inverse(Z),Z)))))),inverse(multiply(multiply(inverse(U),U),inverse(multiply(inverse(V),V)))))) = Y,
inference('PARAMODULATE',[status(thm)],[910,1672,theory(equality)]) ).
cnf(8385,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),multiply(inverse(V),V)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(W),W)),multiply(U,Z))),inverse(inverse(multiply(inverse(X1),X1))))),
inference('PARAMODULATE',[status(thm)],[265,1672,theory(equality)]) ).
cnf(9366,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),inverse(multiply(inverse(V),V))))) = inverse(multiply(inverse(multiply(multiply(inverse(W),W),multiply(U,Z))),inverse(inverse(multiply(inverse(X1),X1))))),
inference('PARAMODULATE',[status(thm)],[265,1675,theory(equality)]) ).
cnf(10865,plain,
multiply(inverse(multiply(inverse(X),X)),multiply(Y,Z)) = multiply(inverse(multiply(inverse(U),U)),multiply(Y,Z)),
inference('PARAMODULATE',[status(thm)],[2484,910,theory(equality)]) ).
cnf(11284,plain,
multiply(inverse(multiply(inverse(X),X)),Y) = multiply(inverse(multiply(inverse(Z),Z)),Y),
inference('PARAMODULATE',[status(thm)],[10865,911,theory(equality)]) ).
cnf(11286,plain,
multiply(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(inverse(Y),inverse(multiply(inverse(Z),Z))))) = Y,
inference('PARAMODULATE',[status(thm)],[911,1066,theory(equality)]) ).
cnf(11307,plain,
multiply(inverse(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,multiply(inverse(Z),Z))))),inverse(multiply(inverse(U),U))) = Y,
inference('PARAMODULATE',[status(thm)],[911,1527,theory(equality)]) ).
cnf(11308,plain,
multiply(inverse(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,multiply(inverse(Z),Z))))),multiply(inverse(U),U)) = Y,
inference('PARAMODULATE',[status(thm)],[911,1674,theory(equality)]) ).
cnf(11321,plain,
multiply(inverse(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,inverse(inverse(multiply(inverse(Z),Z))))))),multiply(inverse(U),U)) = Y,
inference('PARAMODULATE',[status(thm)],[911,1442,theory(equality)]) ).
cnf(11323,plain,
multiply(inverse(inverse(multiply(inverse(multiply(X,inverse(Y))),multiply(X,inverse(multiply(inverse(Z),Z)))))),inverse(multiply(inverse(multiply(inverse(U),U)),inverse(multiply(inverse(V),V))))) = Y,
inference('PARAMODULATE',[status(thm)],[911,908,theory(equality)]) ).
cnf(11335,plain,
multiply(inverse(multiply(X,inverse(multiply(inverse(Y),Y)))),multiply(X,inverse(inverse(multiply(inverse(multiply(Z,inverse(U))),multiply(Z,inverse(inverse(multiply(inverse(V),V))))))))) = U,
inference('PARAMODULATE',[status(thm)],[950,911,theory(equality)]) ).
cnf(11435,plain,
multiply(inverse(inverse(multiply(inverse(multiply(multiply(inverse(X),X),inverse(Y))),inverse(inverse(multiply(inverse(Z),Z)))))),inverse(multiply(multiply(inverse(U),U),inverse(multiply(inverse(V),V))))) = Y,
inference('PARAMODULATE',[status(thm)],[911,1671,theory(equality)]) ).
cnf(11465,plain,
multiply(inverse(inverse(multiply(inverse(multiply(multiply(inverse(X),X),inverse(Y))),inverse(inverse(multiply(inverse(Z),Z)))))),inverse(multiply(inverse(multiply(inverse(U),U)),inverse(multiply(inverse(V),V))))) = Y,
inference('PARAMODULATE',[status(thm)],[911,1675,theory(equality)]) ).
cnf(11624,plain,
multiply(inverse(inverse(multiply(inverse(X),X))),Y) = multiply(inverse(multiply(inverse(Z),Z)),Y),
inference('PARAMODULATE',[status(thm)],[11284,1442,theory(equality)]) ).
cnf(11847,plain,
multiply(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(inverse(Y),multiply(inverse(Z),Z)))) = Y,
inference('PARAMODULATE',[status(thm)],[11286,1442,theory(equality)]) ).
cnf(11850,plain,
multiply(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(inverse(multiply(Y,inverse(multiply(inverse(Z),Z)))),multiply(Y,inverse(U))))) = U,
inference('PARAMODULATE',[status(thm)],[11286,950,theory(equality)]) ).
cnf(11973,plain,
multiply(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(inverse(Y),inverse(multiply(inverse(inverse(multiply(inverse(Z),Z))),inverse(inverse(inverse(multiply(inverse(U),U))))))))) = Y,
inference('PARAMODULATE',[status(thm)],[11286,1673,theory(equality)]) ).
cnf(12176,plain,
multiply(multiply(inverse(X),X),inverse(multiply(inverse(Y),multiply(inverse(Z),Z)))) = Y,
inference('PARAMODULATE',[status(thm)],[11847,1520,theory(equality)]) ).
cnf(12177,plain,
X = multiply(inverse(multiply(inverse(Y),Y)),inverse(multiply(inverse(X),multiply(inverse(Z),Z)))),
inference('PARAMODULATE',[status(thm)],[11624,11847,theory(equality)]) ).
cnf(12182,plain,
multiply(inverse(inverse(multiply(inverse(X),X))),inverse(multiply(inverse(multiply(Y,Z)),multiply(Y,U)))) = multiply(inverse(U),Z),
inference('PARAMODULATE',[status(thm)],[11847,1257,theory(equality)]) ).
cnf(12183,plain,
multiply(inverse(inverse(X)),inverse(multiply(inverse(Y),Y))) = X,
inference('REWRITE',[status(thm)],[11850,12182,theory(equality)]) ).
cnf(12185,plain,
multiply(inverse(multiply(X,inverse(Y))),multiply(X,multiply(inverse(Z),Z))) = Y,
inference('REWRITE',[status(thm)],[11307,12183,theory(equality)]) ).
cnf(12186,plain,
multiply(inverse(inverse(X)),multiply(inverse(Y),Y)) = X,
inference('REWRITE',[status(thm)],[11308,12185,theory(equality)]) ).
cnf(12188,plain,
multiply(inverse(multiply(X,inverse(Y))),multiply(X,inverse(inverse(multiply(inverse(Z),Z))))) = Y,
inference('REWRITE',[status(thm)],[11321,12186,theory(equality)]) ).
cnf(12189,plain,
multiply(inverse(multiply(X,inverse(multiply(inverse(Y),Y)))),multiply(X,inverse(inverse(Z)))) = Z,
inference('REWRITE',[status(thm)],[11335,12188,theory(equality)]) ).
cnf(12190,plain,
inverse(multiply(inverse(multiply(X,Y)),multiply(X,inverse(inverse(multiply(inverse(Z),Z)))))) = Y,
inference('REWRITE',[status(thm)],[1072,12189,theory(equality)]) ).
cnf(12192,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(U),U))) = multiply(inverse(Y),Z),
inference('REWRITE',[status(thm)],[7597,12190,theory(equality)]) ).
cnf(12193,plain,
multiply(inverse(X),Y) = inverse(multiply(inverse(multiply(Z,multiply(U,Y))),multiply(Z,multiply(U,X)))),
inference('REWRITE',[status(thm)],[1275,12192,theory(equality)]) ).
cnf(12297,plain,
inverse(multiply(inverse(multiply(X,multiply(inverse(Y),Z))),multiply(X,multiply(inverse(U),U)))) = multiply(inverse(Y),Z),
inference('REWRITE',[status(thm)],[1277,12193,theory(equality)]) ).
cnf(12298,plain,
inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(multiply(Y,Z)),multiply(Y,U)))) = multiply(inverse(U),Z),
inference('REWRITE',[status(thm)],[7149,12297,theory(equality)]) ).
cnf(12299,plain,
X = inverse(multiply(inverse(multiply(Y,X)),multiply(Y,inverse(multiply(inverse(Z),Z))))),
inference('REWRITE',[status(thm)],[7292,12183,12298,theory(equality)]) ).
cnf(12300,plain,
multiply(inverse(inverse(X)),inverse(multiply(inverse(multiply(inverse(Y),Y)),inverse(multiply(inverse(Z),Z))))) = X,
inference('REWRITE',[status(thm)],[11323,12299,theory(equality)]) ).
cnf(12301,plain,
multiply(inverse(multiply(multiply(inverse(X),X),inverse(Y))),inverse(inverse(multiply(inverse(Z),Z)))) = Y,
inference('REWRITE',[status(thm)],[11465,12300,theory(equality)]) ).
cnf(12302,plain,
multiply(inverse(inverse(X)),inverse(multiply(multiply(inverse(Y),Y),inverse(multiply(inverse(Z),Z))))) = X,
inference('REWRITE',[status(thm)],[11435,12301,theory(equality)]) ).
cnf(12310,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(X),X)),Y)),inverse(inverse(multiply(inverse(Z),Z))))) = Y,
inference('REWRITE',[status(thm)],[8366,12302,theory(equality)]) ).
cnf(12311,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),multiply(inverse(V),V)))) = multiply(U,Z),
inference('REWRITE',[status(thm)],[8385,12310,theory(equality)]) ).
cnf(12312,plain,
multiply(X,Y) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(Z),Z)),multiply(X,Y))),multiply(inverse(U),U))),
inference('REWRITE',[status(thm)],[1370,12311,theory(equality)]) ).
cnf(12313,plain,
inverse(multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,Z))),multiply(inverse(multiply(U,Y)),inverse(multiply(inverse(V),V))))) = multiply(U,Z),
inference('REWRITE',[status(thm)],[1489,12312,theory(equality)]) ).
cnf(12317,plain,
multiply(X,Y) = inverse(multiply(inverse(multiply(multiply(inverse(Z),Z),multiply(X,Y))),multiply(inverse(U),U))),
inference('REWRITE',[status(thm)],[3089,12313,theory(equality)]) ).
cnf(12318,plain,
multiply(X,Y) = inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(Z),Z))),multiply(X,Y))),multiply(inverse(U),U))),
inference('REWRITE',[status(thm)],[3624,12313,theory(equality)]) ).
cnf(12321,plain,
multiply(X,Y) = inverse(multiply(inverse(multiply(multiply(inverse(Z),Z),multiply(X,Y))),inverse(inverse(multiply(inverse(U),U))))),
inference('REWRITE',[status(thm)],[9366,12313,theory(equality)]) ).
cnf(12323,plain,
inverse(multiply(inverse(multiply(inverse(multiply(inverse(X),Y)),Z)),multiply(inverse(multiply(U,Y)),multiply(U,X)))) = Z,
inference('REWRITE',[status(thm)],[8365,12310,theory(equality)]) ).
cnf(12324,plain,
inverse(multiply(inverse(multiply(inverse(X),X)),multiply(inverse(Y),multiply(inverse(Z),Z)))) = Y,
inference('REWRITE',[status(thm)],[7303,12323,theory(equality)]) ).
cnf(12325,plain,
X = inverse(multiply(inverse(multiply(Y,X)),multiply(Y,multiply(inverse(Z),Z)))),
inference('REWRITE',[status(thm)],[7111,12324,theory(equality)]) ).
cnf(12350,plain,
inverse(multiply(inverse(X),inverse(inverse(multiply(inverse(Y),Y))))) = X,
inference('REWRITE',[status(thm)],[6181,12325,theory(equality)]) ).
cnf(12351,plain,
multiply(X,Y) = multiply(multiply(inverse(Z),Z),multiply(X,Y)),
inference('REWRITE',[status(thm)],[12321,12350,theory(equality)]) ).
cnf(12352,plain,
multiply(X,Y) = inverse(multiply(inverse(multiply(X,Y)),multiply(inverse(Z),Z))),
inference('REWRITE',[status(thm)],[12317,12351,theory(equality)]) ).
cnf(12353,plain,
multiply(X,Y) = multiply(inverse(inverse(multiply(inverse(Z),Z))),multiply(X,Y)),
inference('REWRITE',[status(thm)],[12318,12352,theory(equality)]) ).
cnf(12359,plain,
multiply(inverse(multiply(X,multiply(Y,Z))),multiply(X,multiply(Y,U))) = multiply(inverse(multiply(inverse(U),Z)),multiply(inverse(V),V)),
inference('REWRITE',[status(thm)],[5505,12353,theory(equality)]) ).
cnf(12365,plain,
multiply(inverse(multiply(inverse(X),Y)),multiply(inverse(Z),Z)) = multiply(inverse(Y),X),
inference('REWRITE',[status(thm)],[4775,12353,theory(equality)]) ).
cnf(12366,plain,
multiply(inverse(multiply(X,multiply(Y,Z))),multiply(X,multiply(Y,U))) = multiply(inverse(Z),U),
inference('REWRITE',[status(thm)],[12359,12365,theory(equality)]) ).
cnf(12896,plain,
multiply(inverse(multiply(inverse(multiply(X,Y)),multiply(X,multiply(Z,U)))),multiply(inverse(multiply(inverse(multiply(Z,V)),Y)),multiply(inverse(multiply(W,V)),X1))) = multiply(inverse(multiply(W,U)),X1),
inference('REWRITE',[status(thm)],[589,12366,theory(equality)]) ).
cnf(12897,plain,
multiply(inverse(X),Y) = multiply(inverse(multiply(Z,X)),multiply(Z,Y)),
inference('REWRITE',[status(thm)],[4973,12365,12896,theory(equality)]) ).
cnf(12905,plain,
multiply(inverse(inverse(multiply(inverse(X),X))),inverse(inverse(Y))) = Y,
inference('REWRITE',[status(thm)],[12189,12897,theory(equality)]) ).
cnf(12906,plain,
multiply(inverse(inverse(multiply(inverse(X),X))),Y) = Y,
inference('REWRITE',[status(thm)],[11973,12350,12905,theory(equality)]) ).
cnf(12907,plain,
inverse(inverse(X)) = X,
inference('REWRITE',[status(thm)],[12905,12906,theory(equality)]) ).
cnf(12957,plain,
multiply(multiply(inverse(X),X),Y) = Y,
inference('REWRITE',[status(thm)],[12906,12907,theory(equality)]) ).
cnf(12958,plain,
inverse(multiply(inverse(X),multiply(inverse(Y),Y))) = X,
inference('REWRITE',[status(thm)],[12176,12957,theory(equality)]) ).
cnf(12959,plain,
X = multiply(inverse(multiply(inverse(Y),Y)),X),
inference('REWRITE',[status(thm)],[12177,12958,theory(equality)]) ).
cnf(12982,plain,
$false,
inference('REWRITE',[status(thm)],[1519,12959,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : GRP419-1 : TPTP v8.1.0. Released v2.6.0.
% 0.14/0.15 % Command : run-snark %s %d
% 0.15/0.36 % Computer : n023.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 600
% 0.15/0.36 % DateTime : Mon Jun 13 23:54:21 EDT 2022
% 0.15/0.37 % CPUTime :
% 0.22/0.50 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.51 *
% 0.22/0.51 *
% 0.22/0.51 #<PACKAGE "SNARK-USER">
% 0.22/0.51 *
% 0.22/0.51 SNARK-TPTP-OPTIONS
% 0.22/0.51 *
% 0.22/0.51 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.22/0.51 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.22/0.51 (USE-FACTORING :POS)
% 0.22/0.51 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.22/0.51 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.22/0.51 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.22/0.51 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.22/0.51 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.22/0.51 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.22/0.51 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.22/0.51 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.22/0.51 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.22/0.51 (DECLARE-TPTP-SYMBOLS2))
% 0.22/0.51 *
% 0.22/0.51 "."
% 0.22/0.51 *
% 0.22/0.52 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-13T23:54:21
% 0.22/0.52 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n023.cluster.edu at 2022-06-13T23:54:21
% 10.69/10.92
% 10.69/10.92
% 10.69/10.92 #||
% 10.69/10.92 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.69/10.92 % SZS output start Refutation
% See solution above
% 10.82/10.98 ||#
% 10.82/10.98
% 10.82/10.98 ; Summary of computation:
% 10.82/10.98 ; 47147 formulas have been input or derived (from 105 formulas).
% 10.82/10.98 ; 12982 (28%) were retained. Of these,
% 10.82/10.98 ; 12959 (100%) were simplified or subsumed later,
% 10.82/10.98 ; 23 ( 0%) are still being kept.
% 10.82/10.98 ;
% 10.82/10.98 ; Run time in seconds excluding printing time:
% 10.82/10.98 ; 0.001 0% Read assertion file (1 call)
% 10.82/10.98 ; 0.000 0% Assert (2 calls)
% 10.82/10.98 ; 2.585 25% Process new row (36,204 calls)
% 10.82/10.98 ; 0.055 1% Resolution (208 calls)
% 10.82/10.98 ; 0.958 9% Paramodulation (104 calls)
% 10.82/10.98 ; 2.966 29% Forward simplification (34,209 calls)
% 10.82/10.98 ; 3.499 34% Backward simplification (12,982 calls)
% 10.82/10.98 ; 0.212 2% Ordering (67,707 calls)
% 10.82/10.98 ; 0.000 0% Sortal reasoning (32 calls)
% 10.82/10.98 ; 0.000 0% Purity testing (1 call)
% 10.82/10.98 ; 0.129 1% Other
% 10.82/10.98 ; 10.405 Total
% 10.82/10.98 ; 10.470 Real time
% 10.82/10.99 ;
% 10.82/10.99 ; Term-hash-array has 32,332 terms in all.
% 10.82/10.99 ; Feature-vector-row-index has 0 entries (0 at peak, 0 added, 0 deleted).
% 10.82/10.99 ; Feature-vector-row-index has 1 node (1 at peak, 1 added, 0 deleted).
% 10.82/10.99 ; Path-index has 93 entries (26,517 at peak, 33,158 added, 33,065 deleted).
% 10.82/10.99 ; Path-index has 47,938 nodes (59,985 at peak, 71,998 added, 24,060 deleted).
% 10.82/10.99 ; Trie-index has 93 entries (26,517 at peak, 33,158 added, 33,065 deleted).
% 10.82/10.99 ; Trie-index has 389 nodes (257,725 at peak, 375,179 added, 374,790 deleted).
% 10.82/10.99 ; Retrieved 74,332 generalization terms in 348,778 calls.
% 10.82/10.99 ; Retrieved 63,952 instance terms in 13,028 calls.
% 10.82/10.99 ; Retrieved 289,598 unifiable terms in 1,391 calls.
% 10.82/10.99 ;
% 10.82/10.99 ; The agenda of backward simplifiable rows to process has 9951 entries:
% 10.82/10.99 ; 9951 with value 0
% 10.82/10.99 ; The agenda of rows to process has 393 entries:
% 10.82/10.99 ; 7 with value 45 25 with value 54 4 with value 63
% 10.82/10.99 ; 26 with value 46 19 with value 55 4 with value 64
% 10.82/10.99 ; 14 with value 47 31 with value 56 8 with value 65
% 10.82/10.99 ; 20 with value 48 25 with value 57 4 with value 66
% 10.82/10.99 ; 29 with value 49 17 with value 58 9 with value 67
% 10.82/10.99 ; 22 with value 50 11 with value 59 5 with value 68
% 10.82/10.99 ; 34 with value 51 7 with value 60 6 with value 69
% 10.82/10.99 ; 25 with value 52 8 with value 61 4 with value 70
% 10.82/10.99 ; 24 with value 53 5 with value 62
% 10.82/10.99 ; The agenda of rows to give has 21 entries:
% 10.82/10.99 ; 1 with value (4 21) 1 with value (4 32) 1 with value (4 37)
% 10.82/10.99 ; 1 with value (4 25) 2 with value (4 33) 1 with value (4 38)
% 10.82/10.99 ; 1 with value (4 27) 3 with value (4 34) 1 with value (4 39)
% 10.82/10.99 ; 2 with value (4 29) 2 with value (4 35) 1 with value (4 41)
% 10.82/10.99 ; 2 with value (4 31) 1 with value (4 36) 1 with value (4 42)
% 10.82/10.99 Evaluation took:
% 10.82/10.99 10.471 seconds of real time
% 10.82/10.99 9.648548 seconds of user run time
% 10.82/10.99 0.822882 seconds of system run time
% 10.82/10.99 [Run times include 2.571 seconds GC run time.]
% 10.82/10.99 0 calls to %EVAL
% 10.82/10.99 0 page faults and
% 10.82/10.99 605,732,032 bytes consed.
% 10.82/10.99 :PROOF-FOUND
% 10.82/10.99 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-13T23:54:31
% 10.82/10.99 :PROOF-FOUND
% 10.82/10.99 *
%------------------------------------------------------------------------------