%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GRP434-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n015.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:47:27 EDT 2022
% Result : Unsatisfiable 22.83s 23.04s
% Output : Refutation 22.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 2
% Syntax : Number of clauses : 43 ( 43 unt; 0 nHn; 43 RR)
% Number of literals : 43 ( 0 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 17 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(inverse(multiply(multiply(multiply(inverse(multiply(multiply(u,v),w)),u),v),multiply(x,inverse(x)))),w),
file('GRP434-1.p',unknown),
[] ).
cnf(2,axiom,
~ equal(multiply(multiply(inverse(b2),b2),a2),a2),
file('GRP434-1.p',unknown),
[] ).
cnf(4,plain,
equal(inverse(multiply(multiply(multiply(u,multiply(inverse(multiply(multiply(v,w),u)),v)),w),multiply(x,inverse(x)))),multiply(y,inverse(y))),
inference(spr,[status(thm),theory(equality)],[1]),
[iquote('0:SpR:1.0,1.0')] ).
cnf(10,plain,
equal(multiply(u,inverse(u)),multiply(v,inverse(v))),
inference(spr,[status(thm),theory(equality)],[4]),
[iquote('0:SpR:4.0,4.0')] ).
cnf(12,plain,
equal(inverse(multiply(multiply(multiply(inverse(inverse(multiply(multiply(multiply(u,multiply(inverse(multiply(multiply(v,w),u)),v)),w),multiply(x,inverse(x))))),y),z),multiply(x1,inverse(x1)))),inverse(multiply(y,z))),
inference(spr,[status(thm),theory(equality)],[4,1]),
[iquote('0:SpR:4.0,1.0')] ).
cnf(31,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(u,inverse(u))),v),w),multiply(x,inverse(x)))),inverse(multiply(v,w))),
inference(spr,[status(thm),theory(equality)],[10,1]),
[iquote('0:SpR:10.0,1.0')] ).
cnf(37,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(multiply(u,inverse(u)),v)),w),inverse(w)),multiply(x,inverse(x)))),v),
inference(spr,[status(thm),theory(equality)],[10,1]),
[iquote('0:SpR:10.0,1.0')] ).
cnf(108,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(u,inverse(u))),v),inverse(v)),multiply(w,inverse(w)))),inverse(multiply(x,inverse(x)))),
inference(spr,[status(thm),theory(equality)],[10,37]),
[iquote('0:SpR:10.0,37.0')] ).
cnf(112,plain,
equal(inverse(multiply(u,inverse(u))),inverse(multiply(v,inverse(v)))),
inference(rew,[status(thm),theory(equality)],[31,108]),
[iquote('0:Rew:31.0,108.0')] ).
cnf(126,plain,
equal(multiply(u,inverse(u)),multiply(multiply(v,inverse(v)),inverse(multiply(w,inverse(w))))),
inference(spr,[status(thm),theory(equality)],[112,10]),
[iquote('0:SpR:112.0,10.0')] ).
cnf(167,plain,
equal(inverse(multiply(multiply(multiply(multiply(u,inverse(u)),inverse(multiply(v,inverse(v)))),inverse(inverse(inverse(multiply(multiply(w,inverse(w)),x))))),multiply(y,inverse(y)))),x),
inference(spr,[status(thm),theory(equality)],[126,37]),
[iquote('0:SpR:126.0,37.0')] ).
cnf(193,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(u,inverse(u))),multiply(inverse(multiply(v,inverse(v))),w)),inverse(w)),multiply(x,inverse(x)))),multiply(y,inverse(y))),
inference(spr,[status(thm),theory(equality)],[126,4]),
[iquote('0:SpR:126.0,4.0')] ).
cnf(242,plain,
equal(inverse(multiply(multiply(inverse(multiply(u,inverse(u))),v),inverse(v))),multiply(w,inverse(w))),
inference(rew,[status(thm),theory(equality)],[31,193]),
[iquote('0:Rew:31.0,193.0')] ).
cnf(248,plain,
equal(inverse(multiply(multiply(multiply(multiply(u,inverse(u)),inverse(multiply(v,inverse(v)))),w),multiply(x,inverse(x)))),inverse(w)),
inference(spr,[status(thm),theory(equality)],[242,1]),
[iquote('0:SpR:242.0,1.0')] ).
cnf(324,plain,
equal(inverse(inverse(inverse(inverse(multiply(multiply(u,inverse(u)),v))))),v),
inference(rew,[status(thm),theory(equality)],[248,167]),
[iquote('0:Rew:248.0,167.0')] ).
cnf(452,plain,
equal(inverse(inverse(inverse(inverse(multiply(multiply(inverse(inverse(inverse(multiply(multiply(u,inverse(u)),v)))),v),w))))),w),
inference(spr,[status(thm),theory(equality)],[324]),
[iquote('0:SpR:324.0,324.0')] ).
cnf(468,plain,
equal(inverse(inverse(inverse(inverse(multiply(multiply(multiply(u,inverse(u)),inverse(multiply(v,inverse(v)))),w))))),w),
inference(spr,[status(thm),theory(equality)],[112,324]),
[iquote('0:SpR:112.0,324.0')] ).
cnf(473,plain,
equal(inverse(inverse(inverse(inverse(multiply(inverse(multiply(multiply(inverse(multiply(u,inverse(u))),v),inverse(v))),w))))),w),
inference(spr,[status(thm),theory(equality)],[242,324]),
[iquote('0:SpR:242.0,324.0')] ).
cnf(479,plain,
equal(inverse(inverse(inverse(inverse(multiply(u,inverse(u)))))),inverse(multiply(v,inverse(v)))),
inference(spr,[status(thm),theory(equality)],[10,324]),
[iquote('0:SpR:10.0,324.0')] ).
cnf(494,plain,
equal(multiply(u,inverse(u)),multiply(inverse(inverse(inverse(multiply(v,inverse(v))))),inverse(multiply(w,inverse(w))))),
inference(spr,[status(thm),theory(equality)],[479,10]),
[iquote('0:SpR:479.0,10.0')] ).
cnf(546,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(multiply(u,inverse(u)),v)),multiply(w,inverse(w))),inverse(inverse(inverse(inverse(multiply(x,inverse(x))))))),multiply(y,inverse(y)))),v),
inference(spr,[status(thm),theory(equality)],[479,37]),
[iquote('0:SpR:479.0,37.0')] ).
cnf(3600,plain,
equal(inverse(inverse(inverse(inverse(multiply(multiply(inverse(inverse(inverse(multiply(inverse(multiply(multiply(inverse(multiply(u,inverse(u))),v),inverse(v))),w)))),w),x))))),x),
inference(spr,[status(thm),theory(equality)],[242,452]),
[iquote('0:SpR:242.0,452.0')] ).
cnf(3875,plain,
equal(inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(u,multiply(inverse(multiply(multiply(v,w),u)),v)),w),multiply(x,inverse(x)))))),inverse(multiply(y,inverse(y)))))))),multiply(z,inverse(z))),
inference(spr,[status(thm),theory(equality)],[12,468]),
[iquote('0:SpR:12.0,468.0')] ).
cnf(4082,plain,
equal(inverse(multiply(multiply(multiply(inverse(inverse(inverse(multiply(u,inverse(u))))),inverse(multiply(v,inverse(v)))),w),multiply(x,inverse(x)))),inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(y,multiply(inverse(multiply(multiply(z,x1),y)),z)),x1),multiply(x2,inverse(x2)))))),w))),
inference(spr,[status(thm),theory(equality)],[494,12]),
[iquote('0:SpR:494.0,12.0')] ).
cnf(4084,plain,
equal(inverse(multiply(multiply(multiply(multiply(u,inverse(u)),inverse(multiply(v,inverse(v)))),w),multiply(x,inverse(x)))),inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(y,multiply(inverse(multiply(multiply(z,x1),y)),z)),x1),multiply(x2,inverse(x2)))))),w))),
inference(spr,[status(thm),theory(equality)],[126,12]),
[iquote('0:SpR:126.0,12.0')] ).
cnf(4085,plain,
equal(inverse(multiply(multiply(multiply(u,inverse(u)),v),multiply(w,inverse(w)))),inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(x,multiply(inverse(multiply(multiply(y,z),x)),y)),z),multiply(x1,inverse(x1)))))),v))),
inference(spr,[status(thm),theory(equality)],[10,12]),
[iquote('0:SpR:10.0,12.0')] ).
cnf(4102,plain,
equal(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(u,multiply(inverse(multiply(multiply(v,w),u)),v)),w),multiply(x,inverse(x)))))),y)),inverse(y)),
inference(rew,[status(thm),theory(equality)],[248,4084]),
[iquote('0:Rew:248.0,4084.0')] ).
cnf(4105,plain,
equal(inverse(inverse(inverse(inverse(inverse(multiply(u,inverse(u))))))),multiply(v,inverse(v))),
inference(rew,[status(thm),theory(equality)],[4102,3875]),
[iquote('0:Rew:4102.0,3875.0')] ).
cnf(4106,plain,
equal(inverse(multiply(multiply(multiply(u,inverse(u)),v),multiply(w,inverse(w)))),inverse(v)),
inference(rew,[status(thm),theory(equality)],[4102,4085]),
[iquote('0:Rew:4102.0,4085.0')] ).
cnf(4139,plain,
equal(inverse(multiply(multiply(multiply(inverse(inverse(inverse(multiply(u,inverse(u))))),inverse(multiply(v,inverse(v)))),w),multiply(x,inverse(x)))),inverse(w)),
inference(rew,[status(thm),theory(equality)],[4102,4082]),
[iquote('0:Rew:4102.0,4082.0')] ).
cnf(4384,plain,
equal(inverse(inverse(multiply(u,inverse(u)))),multiply(v,inverse(v))),
inference(spr,[status(thm),theory(equality)],[324,4105]),
[iquote('0:SpR:324.0,4105.0')] ).
cnf(4548,plain,
equal(inverse(multiply(multiply(multiply(inverse(inverse(inverse(multiply(u,inverse(u))))),v),w),multiply(x,inverse(x)))),inverse(multiply(v,w))),
inference(spr,[status(thm),theory(equality)],[4384,1]),
[iquote('0:SpR:4384.0,1.0')] ).
cnf(4745,plain,
equal(inverse(multiply(inverse(multiply(u,inverse(u))),v)),inverse(v)),
inference(rew,[status(thm),theory(equality)],[4548,4139]),
[iquote('0:Rew:4548.0,4139.0')] ).
cnf(4846,plain,
equal(inverse(multiply(inverse(multiply(multiply(inverse(multiply(u,inverse(u))),v),inverse(v))),w)),inverse(w)),
inference(spr,[status(thm),theory(equality)],[4745]),
[iquote('0:SpR:4745.0,4745.0')] ).
cnf(5062,plain,
equal(inverse(inverse(inverse(inverse(u)))),u),
inference(rew,[status(thm),theory(equality)],[4846,473]),
[iquote('0:Rew:4846.0,473.0')] ).
cnf(5108,plain,
equal(inverse(inverse(inverse(inverse(multiply(multiply(inverse(inverse(inverse(u))),u),v))))),v),
inference(rew,[status(thm),theory(equality)],[4846,3600]),
[iquote('0:Rew:4846.0,3600.0')] ).
cnf(5168,plain,
equal(multiply(multiply(u,inverse(u)),v),v),
inference(rew,[status(thm),theory(equality)],[5062,324]),
[iquote('0:Rew:5062.0,324.0')] ).
cnf(6006,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(multiply(u,inverse(u)),v)),multiply(w,inverse(w))),multiply(x,inverse(x))),multiply(y,inverse(y)))),v),
inference(rew,[status(thm),theory(equality)],[5062,546]),
[iquote('0:Rew:5062.0,546.0')] ).
cnf(7227,plain,
equal(inverse(multiply(u,multiply(v,inverse(v)))),inverse(u)),
inference(rew,[status(thm),theory(equality)],[5168,4106]),
[iquote('0:Rew:5168.0,4106.0')] ).
cnf(7543,plain,
equal(multiply(multiply(inverse(inverse(inverse(u))),u),v),v),
inference(rew,[status(thm),theory(equality)],[5062,5108]),
[iquote('0:Rew:5062.0,5108.0')] ).
cnf(8541,plain,
equal(inverse(inverse(u)),u),
inference(rew,[status(thm),theory(equality)],[7227,6006,5168]),
[iquote('0:Rew:7227.0,6006.0,7227.0,6006.0,7227.0,6006.0,5168.0,6006.0')] ).
cnf(8573,plain,
equal(multiply(multiply(inverse(u),u),v),v),
inference(rew,[status(thm),theory(equality)],[8541,7543]),
[iquote('0:Rew:8541.0,7543.0')] ).
cnf(8612,plain,
$false,
inference(unc,[status(thm)],[8573,2]),
[iquote('0:UnC:8573.0,2.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GRP434-1 : TPTP v8.1.0. Released v2.6.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Mon Jun 13 21:55:08 EDT 2022
% 0.12/0.34 % CPUTime :
% 22.83/23.04
% 22.83/23.04 SPASS V 3.9
% 22.83/23.04 SPASS beiseite: Proof found.
% 22.83/23.04 % SZS status Theorem
% 22.83/23.04 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.83/23.04 SPASS derived 7531 clauses, backtracked 0 clauses, performed 0 splits and kept 3089 clauses.
% 22.83/23.04 SPASS allocated 84593 KBytes.
% 22.83/23.04 SPASS spent 0:0:22.59 on the problem.
% 22.83/23.04 0:00:00.03 for the input.
% 22.83/23.04 0:00:00.00 for the FLOTTER CNF translation.
% 22.83/23.04 0:00:00.06 for inferences.
% 22.83/23.04 0:00:00.00 for the backtracking.
% 22.83/23.04 0:0:22.47 for the reduction.
% 22.83/23.04
% 22.83/23.04
% 22.83/23.04 Here is a proof with depth 10, length 43 :
% 22.83/23.04 % SZS output start Refutation
% See solution above
% 22.83/23.04 Formulae used in the proof : single_axiom prove_these_axioms_2
% 22.83/23.04
%------------------------------------------------------------------------------