%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GRP563-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n017.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:48:03 EDT 2022
% Result : Unsatisfiable 0.14s 0.48s
% Output : Refutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 3
% Syntax : Number of clauses : 56 ( 56 unt; 0 nHn; 56 RR)
% Number of literals : 56 ( 0 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(divide(divide(divide(u,inverse(v)),w),divide(u,w)),v),
file('GRP563-1.p',unknown),
[] ).
cnf(2,axiom,
equal(divide(u,inverse(v)),multiply(u,v)),
file('GRP563-1.p',unknown),
[] ).
cnf(3,axiom,
~ equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))),
file('GRP563-1.p',unknown),
[] ).
cnf(4,plain,
equal(divide(divide(multiply(u,v),w),divide(u,w)),v),
inference(rew,[status(thm),theory(equality)],[2,1]),
[iquote('0:Rew:2.0,1.0')] ).
cnf(6,plain,
equal(divide(divide(multiply(divide(multiply(u,v),w),x),divide(u,w)),v),x),
inference(spr,[status(thm),theory(equality)],[4]),
[iquote('0:SpR:4.0,4.0')] ).
cnf(8,plain,
equal(divide(divide(multiply(u,v),inverse(w)),multiply(u,w)),v),
inference(spr,[status(thm),theory(equality)],[2,4]),
[iquote('0:SpR:2.0,4.0')] ).
cnf(10,plain,
equal(divide(multiply(multiply(u,v),w),multiply(u,w)),v),
inference(rew,[status(thm),theory(equality)],[2,8]),
[iquote('0:Rew:2.0,8.0')] ).
cnf(13,plain,
equal(divide(u,divide(multiply(v,u),multiply(v,w))),w),
inference(spr,[status(thm),theory(equality)],[10,4]),
[iquote('0:SpR:10.0,4.0')] ).
cnf(15,plain,
equal(divide(divide(multiply(u,v),divide(multiply(w,u),multiply(w,x))),x),v),
inference(spr,[status(thm),theory(equality)],[13,4]),
[iquote('0:SpR:13.0,4.0')] ).
cnf(18,plain,
equal(multiply(divide(multiply(divide(multiply(u,inverse(v)),w),x),divide(u,w)),v),x),
inference(spr,[status(thm),theory(equality)],[6,2]),
[iquote('0:SpR:6.0,2.0')] ).
cnf(56,plain,
equal(divide(divide(u,divide(divide(multiply(v,inverse(w)),x),divide(v,x))),u),w),
inference(spr,[status(thm),theory(equality)],[18,6]),
[iquote('0:SpR:18.0,6.0')] ).
cnf(57,plain,
equal(multiply(divide(inverse(u),divide(divide(multiply(v,inverse(w)),x),divide(v,x))),u),w),
inference(spr,[status(thm),theory(equality)],[18]),
[iquote('0:SpR:18.0,18.0')] ).
cnf(71,plain,
equal(multiply(divide(multiply(u,v),divide(w,divide(multiply(x,multiply(w,inverse(y))),multiply(x,u)))),y),v),
inference(spr,[status(thm),theory(equality)],[13,18]),
[iquote('0:SpR:13.0,18.0')] ).
cnf(74,plain,
equal(divide(multiply(u,v),u),v),
inference(rew,[status(thm),theory(equality)],[2,56,4]),
[iquote('0:Rew:2.0,56.0,4.0,56.0')] ).
cnf(75,plain,
equal(multiply(multiply(inverse(u),v),u),v),
inference(rew,[status(thm),theory(equality)],[2,57,4]),
[iquote('0:Rew:2.0,57.0,4.0,57.0')] ).
cnf(82,plain,
equal(divide(u,divide(v,v)),u),
inference(spr,[status(thm),theory(equality)],[74,4]),
[iquote('0:SpR:74.0,4.0')] ).
cnf(98,plain,
equal(multiply(divide(u,u),v),v),
inference(spr,[status(thm),theory(equality)],[82,74]),
[iquote('0:SpR:82.0,74.0')] ).
cnf(119,plain,
equal(divide(multiply(u,v),multiply(divide(w,w),v)),u),
inference(spr,[status(thm),theory(equality)],[98,10]),
[iquote('0:SpR:98.0,10.0')] ).
cnf(126,plain,
equal(divide(u,divide(multiply(divide(v,v),u),w)),w),
inference(spr,[status(thm),theory(equality)],[98,13]),
[iquote('0:SpR:98.0,13.0')] ).
cnf(138,plain,
equal(divide(multiply(u,v),v),u),
inference(rew,[status(thm),theory(equality)],[98,119]),
[iquote('0:Rew:98.0,119.0')] ).
cnf(140,plain,
equal(divide(u,divide(u,v)),v),
inference(rew,[status(thm),theory(equality)],[98,126]),
[iquote('0:Rew:98.0,126.0')] ).
cnf(155,plain,
equal(multiply(divide(multiply(u,v),divide(u,inverse(w))),w),v),
inference(spr,[status(thm),theory(equality)],[138,18]),
[iquote('0:SpR:138.0,18.0')] ).
cnf(164,plain,
equal(divide(multiply(u,v),multiply(u,w)),divide(v,w)),
inference(spr,[status(thm),theory(equality)],[138,15]),
[iquote('0:SpR:138.0,15.0')] ).
cnf(165,plain,
equal(divide(multiply(divide(multiply(u,inverse(v)),w),x),divide(u,w)),divide(x,v)),
inference(spr,[status(thm),theory(equality)],[18,138]),
[iquote('0:SpR:18.0,138.0')] ).
cnf(181,plain,
equal(multiply(divide(multiply(u,v),divide(w,divide(multiply(w,inverse(x)),u))),x),v),
inference(rew,[status(thm),theory(equality)],[164,71]),
[iquote('0:Rew:164.0,71.0')] ).
cnf(191,plain,
equal(multiply(divide(multiply(u,v),multiply(u,w)),w),v),
inference(rew,[status(thm),theory(equality)],[2,155]),
[iquote('0:Rew:2.0,155.0')] ).
cnf(192,plain,
equal(multiply(divide(u,v),v),u),
inference(rew,[status(thm),theory(equality)],[164,191]),
[iquote('0:Rew:164.0,191.0')] ).
cnf(264,plain,
equal(divide(u,multiply(u,v)),inverse(v)),
inference(spr,[status(thm),theory(equality)],[2,140]),
[iquote('0:SpR:2.0,140.0')] ).
cnf(380,plain,
equal(multiply(multiply(u,v),inverse(v)),u),
inference(spr,[status(thm),theory(equality)],[2,192]),
[iquote('0:SpR:2.0,192.0')] ).
cnf(384,plain,
equal(multiply(u,v),multiply(v,u)),
inference(spr,[status(thm),theory(equality)],[74,192]),
[iquote('0:SpR:74.0,192.0')] ).
cnf(386,plain,
equal(multiply(multiply(u,v),w),multiply(v,multiply(u,w))),
inference(spr,[status(thm),theory(equality)],[10,192]),
[iquote('0:SpR:10.0,192.0')] ).
cnf(387,plain,
equal(multiply(u,divide(v,w)),divide(multiply(v,u),w)),
inference(spr,[status(thm),theory(equality)],[4,192]),
[iquote('0:SpR:4.0,192.0')] ).
cnf(388,plain,
equal(divide(multiply(divide(multiply(u,v),w),x),divide(u,w)),multiply(x,v)),
inference(spr,[status(thm),theory(equality)],[6,192]),
[iquote('0:SpR:6.0,192.0')] ).
cnf(393,plain,
~ equal(multiply(c3,multiply(a3,b3)),multiply(a3,multiply(b3,c3))),
inference(rew,[status(thm),theory(equality)],[384,3]),
[iquote('0:Rew:384.0,3.0')] ).
cnf(400,plain,
equal(multiply(u,divide(multiply(v,w),divide(x,divide(multiply(x,inverse(u)),v)))),w),
inference(rew,[status(thm),theory(equality)],[384,181]),
[iquote('0:Rew:384.0,181.0')] ).
cnf(416,plain,
equal(multiply(u,multiply(inverse(u),v)),v),
inference(rew,[status(thm),theory(equality)],[384,75]),
[iquote('0:Rew:384.0,75.0')] ).
cnf(417,plain,
equal(multiply(inverse(u),multiply(v,u)),v),
inference(rew,[status(thm),theory(equality)],[384,380]),
[iquote('0:Rew:384.0,380.0')] ).
cnf(442,plain,
equal(multiply(u,inverse(v)),divide(u,v)),
inference(rew,[status(thm),theory(equality)],[388,165]),
[iquote('0:Rew:388.0,165.0')] ).
cnf(461,plain,
equal(divide(multiply(u,multiply(v,w)),divide(x,divide(divide(x,w),v))),u),
inference(rew,[status(thm),theory(equality)],[386,400,387,442]),
[iquote('0:Rew:386.0,400.0,387.0,400.0,442.0,400.0')] ).
cnf(510,plain,
equal(divide(divide(u,u),v),inverse(v)),
inference(spr,[status(thm),theory(equality)],[98,264]),
[iquote('0:SpR:98.0,264.0')] ).
cnf(529,plain,
equal(divide(inverse(u),v),inverse(multiply(v,u))),
inference(spr,[status(thm),theory(equality)],[417,264]),
[iquote('0:SpR:417.0,264.0')] ).
cnf(595,plain,
equal(multiply(inverse(u),v),divide(v,u)),
inference(spr,[status(thm),theory(equality)],[416,74]),
[iquote('0:SpR:416.0,74.0')] ).
cnf(597,plain,
equal(inverse(multiply(inverse(u),v)),divide(u,v)),
inference(spr,[status(thm),theory(equality)],[416,264]),
[iquote('0:SpR:416.0,264.0')] ).
cnf(622,plain,
equal(inverse(divide(u,v)),divide(v,u)),
inference(rew,[status(thm),theory(equality)],[595,597]),
[iquote('0:Rew:595.0,597.0')] ).
cnf(778,plain,
equal(multiply(u,divide(v,w)),divide(u,divide(w,v))),
inference(spr,[status(thm),theory(equality)],[622,2]),
[iquote('0:SpR:622.0,2.0')] ).
cnf(799,plain,
equal(divide(multiply(u,v),w),divide(v,divide(w,u))),
inference(rew,[status(thm),theory(equality)],[387,778]),
[iquote('0:Rew:387.0,778.0')] ).
cnf(818,plain,
equal(divide(multiply(u,v),divide(divide(w,divide(divide(w,v),u)),x)),x),
inference(rew,[status(thm),theory(equality)],[799,461]),
[iquote('0:Rew:799.0,461.0')] ).
cnf(887,plain,
equal(divide(u,divide(divide(divide(v,divide(divide(v,u),w)),x),w)),x),
inference(rew,[status(thm),theory(equality)],[799,818]),
[iquote('0:Rew:799.0,818.0')] ).
cnf(1078,plain,
equal(multiply(divide(u,divide(divide(u,v),w)),x),divide(v,divide(inverse(x),w))),
inference(spr,[status(thm),theory(equality)],[264,887]),
[iquote('0:SpR:264.0,887.0')] ).
cnf(1084,plain,
equal(divide(u,divide(divide(u,v),w)),divide(v,inverse(w))),
inference(spr,[status(thm),theory(equality)],[510,887]),
[iquote('0:SpR:510.0,887.0')] ).
cnf(1091,plain,
equal(divide(u,divide(divide(u,v),w)),multiply(v,w)),
inference(rew,[status(thm),theory(equality)],[2,1084]),
[iquote('0:Rew:2.0,1084.0')] ).
cnf(1160,plain,
equal(multiply(divide(u,divide(divide(u,v),w)),x),multiply(v,multiply(w,x))),
inference(rew,[status(thm),theory(equality)],[2,1078,529]),
[iquote('0:Rew:2.0,1078.0,529.0,1078.0')] ).
cnf(1161,plain,
equal(multiply(u,multiply(v,w)),multiply(v,multiply(u,w))),
inference(rew,[status(thm),theory(equality)],[386,1160,1091]),
[iquote('0:Rew:386.0,1160.0,1091.0,1160.0')] ).
cnf(1162,plain,
~ equal(multiply(a3,multiply(c3,b3)),multiply(a3,multiply(b3,c3))),
inference(rew,[status(thm),theory(equality)],[1161,393]),
[iquote('0:Rew:1161.0,393.0')] ).
cnf(1163,plain,
~ equal(multiply(a3,multiply(b3,c3)),multiply(a3,multiply(b3,c3))),
inference(rew,[status(thm),theory(equality)],[384,1162]),
[iquote('0:Rew:384.0,1162.0')] ).
cnf(1164,plain,
$false,
inference(obv,[status(thm),theory(equality)],[1163]),
[iquote('0:Obv:1163.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : GRP563-1 : TPTP v8.1.0. Released v2.6.0.
% 0.02/0.09 % Command : run_spass %d %s
% 0.09/0.29 % Computer : n017.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 600
% 0.09/0.29 % DateTime : Mon Jun 13 16:50:23 EDT 2022
% 0.09/0.29 % CPUTime :
% 0.14/0.48
% 0.14/0.48 SPASS V 3.9
% 0.14/0.48 SPASS beiseite: Proof found.
% 0.14/0.48 % SZS status Theorem
% 0.14/0.48 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.48 SPASS derived 660 clauses, backtracked 0 clauses, performed 0 splits and kept 215 clauses.
% 0.14/0.48 SPASS allocated 64693 KBytes.
% 0.14/0.48 SPASS spent 0:00:00.17 on the problem.
% 0.14/0.48 0:00:00.03 for the input.
% 0.14/0.48 0:00:00.00 for the FLOTTER CNF translation.
% 0.14/0.48 0:00:00.01 for inferences.
% 0.14/0.48 0:00:00.00 for the backtracking.
% 0.14/0.48 0:00:00.12 for the reduction.
% 0.14/0.48
% 0.14/0.48
% 0.14/0.48 Here is a proof with depth 9, length 56 :
% 0.14/0.48 % SZS output start Refutation
% See solution above
% 0.14/0.48 Formulae used in the proof : single_axiom multiply prove_these_axioms_3
% 0.14/0.48
%------------------------------------------------------------------------------