%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP508-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Sun Sep 27 07:30:15 AM UTC 2026
% Result : Unsatisfiable 47.04s 7.18s
% Output : CNFRefutation 47.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 2
% Syntax : Number of formulae : 61 ( 61 unt; 0 def)
% Number of atoms : 61 ( 60 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 1 avg)
% Maximal term depth : 18 ( 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 : 335 ( 0 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(VAR_0,VAR_1)),multiply(VAR_1,VAR_0))),multiply(inverse(multiply(VAR_2,VAR_3)),multiply(VAR_2,inverse(multiply(multiply(VAR_4,inverse(VAR_5)),inverse(VAR_3))))))),VAR_5) = VAR_4,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(F)),inverse(D))))))),F) = E,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(prove_these_axioms_4,axiom,
multiply(a,b) != multiply(b,a),
file('theBenchmark.p',prove_these_axioms_4) ).
cnf(c_2,plain,
multiply(a,b) != multiply(b,a),
inference(clausify,[status(thm)],[prove_these_axioms_4]) ).
cnf(c_3,plain,
multiply(b,a) != multiply(a,b),
inference(copy,[status(thm)],[c_2]) ).
cnf(c_12803,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),F) = inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(multiply(E,inverse(inverse(F))),inverse(V9))))))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_7,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(F))),inverse(D))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(E,inverse(V9))))))),F),
inference(copy,[status(thm)],[c_12803]) ).
cnf(c_9,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),F),inverse(F)) = E,
inference(paramod,[status(thm)],[c_7,c_1]) ).
cnf(c_10,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,inverse(F)),inverse(inverse(F))),inverse(D))))))) = E,
inference(paramod,[status(thm)],[c_7,c_1]) ).
cnf(c_12804,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(E))))),D) = inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F))),multiply(inverse(multiply(V7,V8)),multiply(V7,inverse(multiply(E,inverse(V8))))))),
inference(paramod,[status(thm)],[c_9,c_1]) ).
cnf(c_15,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F))),multiply(inverse(multiply(V7,inverse(V8))),multiply(V7,inverse(E))))),V8),
inference(copy,[status(thm)],[c_12804]) ).
cnf(c_12805,plain,
multiply(multiply(A,B),inverse(B)) = multiply(multiply(A,inverse(C)),inverse(inverse(C))),
inference(paramod,[status(thm)],[c_10,c_9]) ).
cnf(c_34,plain,
multiply(multiply(A,inverse(B)),inverse(inverse(B))) = multiply(multiply(A,C),inverse(C)),
inference(copy,[status(thm)],[c_12805]) ).
cnf(c_12806,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(multiply(multiply(F,inverse(V10)),inverse(inverse(V10))),inverse(V9))))))))),inverse(D))))))) = E,
inference(paramod,[status(thm)],[c_10,c_10]) ).
cnf(c_36,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(F)),inverse(D))))))) = E,
inference(paramod,[status(thm)],[c_10,c_12806]) ).
cnf(c_40,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(multiply(E,F),inverse(F))))))),D) = E,
inference(paramod,[status(thm)],[c_34,c_1]) ).
cnf(c_61,plain,
multiply(multiply(A,B),inverse(B)) = multiply(multiply(A,C),inverse(C)),
inference(paramod,[status(thm)],[c_34,c_34]) ).
cnf(c_71,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,F),inverse(F))))))),V6),inverse(V6)) = multiply(E,D),
inference(paramod,[status(thm)],[c_61,c_9]) ).
cnf(c_75,plain,
multiply(multiply(multiply(A,B),inverse(B)),inverse(inverse(C))) = multiply(multiply(multiply(A,C),D),inverse(D)),
inference(paramod,[status(thm)],[c_61,c_61]) ).
cnf(c_122,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(C,D),inverse(D))),multiply(multiply(C,E),inverse(multiply(multiply(F,V6),inverse(V6))))))),E) = F,
inference(paramod,[status(thm)],[c_61,c_40]) ).
cnf(c_12807,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(multiply(E,F)),multiply(E,inverse(multiply(V6,inverse(F))))))),V7),inverse(V7))),V6))),multiply(multiply(V8,V9),inverse(V9))) = V8,
inference(paramod,[status(thm)],[c_9,c_122]) ).
cnf(c_379,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),multiply(multiply(D,E),inverse(E))) = D,
inference(paramod,[status(thm)],[c_9,c_12807]) ).
cnf(c_12808,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(C))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(E,D))),multiply(inverse(F),F))),C),V6),inverse(V6)),
inference(paramod,[status(thm)],[c_379,c_75]) ).
cnf(c_415,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D),E),inverse(E)) = multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(inverse(D))),
inference(copy,[status(thm)],[c_12808]) ).
cnf(c_462,plain,
multiply(A,inverse(multiply(multiply(A,B),inverse(B)))) = multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),
inference(paramod,[status(thm)],[c_379,c_71]) ).
cnf(c_12809,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(multiply(E,F)),multiply(E,inverse(multiply(V6,inverse(F))))))),V7),inverse(V7))))) = V6,
inference(paramod,[status(thm)],[c_462,c_9]) ).
cnf(c_501,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(C))) = C,
inference(paramod,[status(thm)],[c_9,c_12809]) ).
cnf(c_547,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D),E),inverse(E)) = D,
inference(paramod,[status(thm)],[c_501,c_415]) ).
cnf(c_12810,plain,
multiply(A,inverse(inverse(inverse(A)))) = multiply(multiply(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))),D),inverse(D)),
inference(paramod,[status(thm)],[c_501,c_61]) ).
cnf(c_562,plain,
multiply(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),C),inverse(C)) = multiply(D,inverse(inverse(inverse(D)))),
inference(copy,[status(thm)],[c_12810]) ).
cnf(c_697,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(F,E))),multiply(inverse(V6),V6))),D),
inference(paramod,[status(thm)],[c_547,c_379]) ).
cnf(c_12811,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E)))))),F),inverse(F)) = multiply(V6,inverse(inverse(inverse(V6)))),
inference(paramod,[status(thm)],[c_379,c_562]) ).
cnf(c_800,plain,
inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))) = multiply(C,inverse(inverse(inverse(C)))),
inference(paramod,[status(thm)],[c_547,c_12811]) ).
cnf(c_12812,plain,
multiply(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),C),inverse(C)) = inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E))))),
inference(paramod,[status(thm)],[c_562,c_501]) ).
cnf(c_805,plain,
inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))) = multiply(multiply(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),E),inverse(E)),
inference(copy,[status(thm)],[c_12812]) ).
cnf(c_2045,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(E))))),D),F),inverse(F)) = E,
inference(paramod,[status(thm)],[c_15,c_9]) ).
cnf(c_12813,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(F,E))),multiply(inverse(V6),V6))),inverse(V7)),inverse(D))))))),V7) = inverse(multiply(inverse(multiply(inverse(multiply(V8,V9)),multiply(V9,V8))),multiply(inverse(V10),V10))),
inference(paramod,[status(thm)],[c_697,c_1]) ).
cnf(c_8144,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))) = inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(E,D))),multiply(inverse(F),F))),
inference(paramod,[status(thm)],[c_1,c_12813]) ).
cnf(c_12814,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(E),E))))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F))),multiply(inverse(V7),V7)),
inference(paramod,[status(thm)],[c_8144,c_501]) ).
cnf(c_8390,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(multiply(D,E)),multiply(E,D))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_501,c_12814]) ).
cnf(c_8598,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(E),E)))),F),V6),inverse(V6)) = F,
inference(paramod,[status(thm)],[c_8390,c_547]) ).
cnf(c_9175,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),inverse(E))),F))),E),V6),inverse(V6)) = inverse(F),
inference(paramod,[status(thm)],[c_501,c_2045]) ).
cnf(c_9203,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),inverse(multiply(E,inverse(multiply(multiply(E,F),inverse(F)))))))),D),V6),inverse(V6)) = inverse(inverse(C)),
inference(paramod,[status(thm)],[c_800,c_2045]) ).
cnf(c_12815,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),E),inverse(F))),inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))))))),F),V8),inverse(V8)) = E,
inference(paramod,[status(thm)],[c_805,c_2045]) ).
cnf(c_9224,plain,
inverse(inverse(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),C))) = C,
inference(paramod,[status(thm)],[c_9203,c_12815]) ).
cnf(c_9487,plain,
multiply(multiply(A,inverse(multiply(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))),D))),D) = multiply(multiply(A,E),inverse(E)),
inference(paramod,[status(thm)],[c_9224,c_61]) ).
cnf(c_12816,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(F)),inverse(D))))))),V6) = multiply(E,inverse(multiply(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))),inverse(V6)))),
inference(paramod,[status(thm)],[c_9487,c_1]) ).
cnf(c_12817,plain,
multiply(E,V6) = multiply(E,inverse(multiply(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))),inverse(V6)))),
inference(paramod,[status(thm)],[c_36,c_12816]) ).
cnf(c_10160,plain,
multiply(A,inverse(multiply(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))),inverse(D)))) = multiply(A,D),
inference(copy,[status(thm)],[c_12817]) ).
cnf(c_12818,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D),E),inverse(E)) = inverse(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(D))),
inference(paramod,[status(thm)],[c_10160,c_547]) ).
cnf(c_12819,plain,
D = inverse(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(D))),
inference(paramod,[status(thm)],[c_547,c_12818]) ).
cnf(c_10701,plain,
inverse(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(C))) = C,
inference(copy,[status(thm)],[c_12819]) ).
cnf(c_10871,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(C,D))),C),E),inverse(E)) = inverse(D),
inference(paramod,[status(thm)],[c_10701,c_9175]) ).
cnf(c_12820,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(E),E)))),inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F)))),V7),inverse(V7)) = inverse(multiply(inverse(V8),V8)),
inference(paramod,[status(thm)],[c_8390,c_10871]) ).
cnf(c_11898,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(B,A))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_8598,c_12820]) ).
cnf(c_12119,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),C),D),inverse(D)) = C,
inference(paramod,[status(thm)],[c_11898,c_547]) ).
cnf(c_12821,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),inverse(multiply(C,D))),E),inverse(E)) = inverse(multiply(D,C)),
inference(paramod,[status(thm)],[c_11898,c_10871]) ).
cnf(c_12629,plain,
inverse(multiply(A,B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_12119,c_12821]) ).
cnf(c_12822,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(C,D)))) = multiply(D,C),
inference(paramod,[status(thm)],[c_12629,c_501]) ).
cnf(c_12801,plain,
multiply(A,B) = multiply(B,A),
inference(paramod,[status(thm)],[c_501,c_12822]) ).
cnf(c_12802,plain,
$false,
inference(resolve,[status(thm)],[c_12801,c_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP508-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n016.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 15:02:45 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.36 % Process 2690417 was started by sandbox on n016,
% 0.02/0.36 % Fri Sep 25 15:02:45 2026
% 0.02/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.02/0.36
% 0.02/0.36 % From the command line: assign(max_seconds, 300).
% 47.04/7.18
% 47.04/7.18 % SZS status Unsatisfiable for theBenchmark
% 47.04/7.18
% 47.04/7.18 % Proof 1 at 5.65 (+ 1.03) seconds.
% 47.04/7.18 % Length of proof is 39.
% 47.04/7.18 % Level of proof is 21.
% 47.04/7.18 % Maximum clause weight is 93.000.
% 47.04/7.18 % Given clauses 107.
% 47.04/7.18
% 47.04/7.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------