%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : BOO002-2 : TPTP v8.1.0. Released v1.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n029.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 : Thu Jul 14 23:49:21 EDT 2022
% Result : Unsatisfiable 100.75s 100.92s
% Output : Refutation 100.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 6
% Syntax : Number of clauses : 35 ( 35 unt; 0 nHn; 35 RR)
% Number of literals : 35 ( 0 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(multiply(multiply(u,v,w),x,multiply(u,v,y)),multiply(u,v,multiply(w,x,y))),
file('BOO002-2.p',unknown),
[] ).
cnf(2,axiom,
equal(multiply(u,v,v),v),
file('BOO002-2.p',unknown),
[] ).
cnf(3,axiom,
equal(multiply(u,u,v),u),
file('BOO002-2.p',unknown),
[] ).
cnf(4,axiom,
equal(multiply(inverse(u),u,v),v),
file('BOO002-2.p',unknown),
[] ).
cnf(5,axiom,
equal(multiply(u,v,u),u),
file('BOO002-2.p',unknown),
[] ).
cnf(6,axiom,
~ equal(multiply(a,inverse(a),b),b),
file('BOO002-2.p',unknown),
[] ).
cnf(19,plain,
equal(multiply(u,v,multiply(w,multiply(u,v,w),x)),multiply(u,v,w)),
inference(spr,[status(thm),theory(equality)],[1,3]),
[iquote('0:SpR:1.0,3.0')] ).
cnf(22,plain,
equal(multiply(multiply(u,v,w),x,u),multiply(u,v,multiply(w,x,u))),
inference(spr,[status(thm),theory(equality)],[5,1]),
[iquote('0:SpR:5.0,1.0')] ).
cnf(24,plain,
equal(multiply(multiply(u,v,w),x,v),multiply(u,v,multiply(w,x,v))),
inference(spr,[status(thm),theory(equality)],[2,1]),
[iquote('0:SpR:2.0,1.0')] ).
cnf(48,plain,
equal(multiply(u,v,multiply(u,v,w)),multiply(u,v,w)),
inference(spr,[status(thm),theory(equality)],[2,19]),
[iquote('0:SpR:2.0,19.0')] ).
cnf(58,plain,
equal(multiply(multiply(u,v,w),x,multiply(u,v,y)),multiply(u,v,multiply(w,x,multiply(u,v,y)))),
inference(spr,[status(thm),theory(equality)],[48,1]),
[iquote('0:SpR:48.0,1.0')] ).
cnf(74,plain,
equal(multiply(u,v,multiply(w,x,multiply(u,v,y))),multiply(u,v,multiply(w,x,y))),
inference(rew,[status(thm),theory(equality)],[1,58]),
[iquote('0:Rew:1.0,58.0')] ).
cnf(190,plain,
equal(multiply(u,v,multiply(u,w,v)),multiply(u,w,v)),
inference(spr,[status(thm),theory(equality)],[5,24]),
[iquote('0:SpR:5.0,24.0')] ).
cnf(199,plain,
equal(multiply(multiply(u,v,multiply(w,x,u)),y,x),multiply(multiply(u,v,w),x,multiply(u,y,x))),
inference(spr,[status(thm),theory(equality)],[22,24]),
[iquote('0:SpR:22.0,24.0')] ).
cnf(673,plain,
equal(multiply(u,multiply(v,w,u),multiply(v,w,u)),multiply(u,multiply(v,w,u),multiply(v,w,x))),
inference(spr,[status(thm),theory(equality)],[19,74]),
[iquote('0:SpR:19.0,74.0')] ).
cnf(704,plain,
equal(multiply(u,multiply(v,w,u),multiply(v,w,x)),multiply(v,w,u)),
inference(rew,[status(thm),theory(equality)],[2,673]),
[iquote('0:Rew:2.0,673.0')] ).
cnf(776,plain,
equal(multiply(u,multiply(v,w,u),v),multiply(v,w,u)),
inference(spr,[status(thm),theory(equality)],[5,704]),
[iquote('0:SpR:5.0,704.0')] ).
cnf(788,plain,
equal(multiply(u,multiply(v,w,u),w),multiply(v,w,u)),
inference(spr,[status(thm),theory(equality)],[2,704]),
[iquote('0:SpR:2.0,704.0')] ).
cnf(1012,plain,
equal(multiply(u,multiply(v,w,u),multiply(v,x,u)),multiply(multiply(v,w,u),x,u)),
inference(spr,[status(thm),theory(equality)],[776,22]),
[iquote('0:SpR:776.0,22.0')] ).
cnf(1129,plain,
equal(multiply(u,multiply(v,u,w),w),multiply(v,u,w)),
inference(spr,[status(thm),theory(equality)],[788,776]),
[iquote('0:SpR:788.0,776.0')] ).
cnf(7002,plain,
equal(multiply(multiply(u,v,inverse(w)),w,multiply(u,x,w)),multiply(multiply(u,v,u),x,w)),
inference(spr,[status(thm),theory(equality)],[4,199]),
[iquote('0:SpR:4.0,199.0')] ).
cnf(7070,plain,
equal(multiply(multiply(u,v,inverse(w)),w,multiply(u,x,w)),multiply(u,x,w)),
inference(rew,[status(thm),theory(equality)],[5,7002]),
[iquote('0:Rew:5.0,7002.0')] ).
cnf(8263,plain,
equal(multiply(multiply(inverse(u),v,w),u,multiply(w,x,u)),multiply(w,x,u)),
inference(spr,[status(thm),theory(equality)],[776,7070]),
[iquote('0:SpR:776.0,7070.0')] ).
cnf(9315,plain,
equal(multiply(multiply(inverse(u),v,w),u,w),w),
inference(spr,[status(thm),theory(equality)],[3,8263]),
[iquote('0:SpR:3.0,8263.0')] ).
cnf(9604,plain,
equal(multiply(multiply(u,inverse(v),w),v,w),w),
inference(spr,[status(thm),theory(equality)],[1129,9315]),
[iquote('0:SpR:1129.0,9315.0')] ).
cnf(25800,plain,
equal(multiply(u,multiply(v,w,u),multiply(multiply(v,x,u),y,u)),multiply(multiply(multiply(v,w,u),x,u),y,u)),
inference(spr,[status(thm),theory(equality)],[1012,22]),
[iquote('0:SpR:1012.0,22.0')] ).
cnf(25822,plain,
equal(multiply(multiply(u,v,w),v,w),multiply(u,v,w)),
inference(spr,[status(thm),theory(equality)],[1012,2]),
[iquote('0:SpR:1012.0,2.0')] ).
cnf(25823,plain,
equal(multiply(u,multiply(v,w,u),multiply(multiply(v,x,u),w,u)),multiply(multiply(v,x,u),w,u)),
inference(spr,[status(thm),theory(equality)],[1012,190]),
[iquote('0:SpR:1012.0,190.0')] ).
cnf(26209,plain,
equal(multiply(multiply(multiply(u,v,w),x,w),v,w),multiply(multiply(u,x,w),v,w)),
inference(rew,[status(thm),theory(equality)],[25800,25823]),
[iquote('0:Rew:25800.0,25823.0')] ).
cnf(26633,plain,
equal(multiply(u,multiply(multiply(v,w,u),x,u),multiply(v,w,u)),multiply(multiply(multiply(v,w,u),x,u),w,u)),
inference(spr,[status(thm),theory(equality)],[25822,1012]),
[iquote('0:SpR:25822.0,1012.0')] ).
cnf(26822,plain,
equal(multiply(multiply(multiply(u,v,w),x,w),v,w),multiply(multiply(u,v,w),x,w)),
inference(rew,[status(thm),theory(equality)],[776,26633]),
[iquote('0:Rew:776.0,26633.0')] ).
cnf(26823,plain,
equal(multiply(multiply(u,v,w),x,w),multiply(multiply(u,x,w),v,w)),
inference(rew,[status(thm),theory(equality)],[26209,26822]),
[iquote('0:Rew:26209.0,26822.0')] ).
cnf(26824,plain,
equal(multiply(multiply(u,v,w),inverse(v),w),w),
inference(rew,[status(thm),theory(equality)],[26823,9604]),
[iquote('0:Rew:26823.0,9604.0')] ).
cnf(28381,plain,
equal(multiply(u,inverse(u),v),v),
inference(spr,[status(thm),theory(equality)],[3,26824]),
[iquote('0:SpR:3.0,26824.0')] ).
cnf(28444,plain,
$false,
inference(unc,[status(thm)],[28381,6]),
[iquote('0:UnC:28381.0,6.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : BOO002-2 : TPTP v8.1.0. Released v1.1.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.12/0.32 % Computer : n029.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 600
% 0.12/0.32 % DateTime : Wed Jun 1 19:54:46 EDT 2022
% 0.12/0.32 % CPUTime :
% 100.75/100.92
% 100.75/100.92 SPASS V 3.9
% 100.75/100.92 SPASS beiseite: Proof found.
% 100.75/100.92 % SZS status Theorem
% 100.75/100.92 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 100.75/100.92 SPASS derived 19178 clauses, backtracked 0 clauses, performed 0 splits and kept 6143 clauses.
% 100.75/100.92 SPASS allocated 109849 KBytes.
% 100.75/100.92 SPASS spent 0:1:39.72 on the problem.
% 100.75/100.92 0:00:00.04 for the input.
% 100.75/100.92 0:00:00.00 for the FLOTTER CNF translation.
% 100.75/100.92 0:00:00.19 for inferences.
% 100.75/100.92 0:00:00.00 for the backtracking.
% 100.75/100.92 0:1:39.45 for the reduction.
% 100.75/100.92
% 100.75/100.92
% 100.75/100.92 Here is a proof with depth 9, length 35 :
% 100.75/100.92 % SZS output start Refutation
% See solution above
% 100.75/100.92 Formulae used in the proof : associativity ternary_multiply_1 ternary_multiply_2 left_inverse extra_lemma prove_equation
% 100.75/100.92
%------------------------------------------------------------------------------