%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GRP040-3 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n008.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:44:57 EDT 2022
% Result : Unsatisfiable 0.47s 0.69s
% Output : Refutation 0.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 16
% Syntax : Number of clauses : 66 ( 30 unt; 4 nHn; 66 RR)
% Number of literals : 124 ( 0 equ; 56 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( subgroup_member(u)
| subgroup_member(v)
| subgroup_member(element_in_O2(u,v)) ),
file('GRP040-3.p',unknown),
[] ).
cnf(2,axiom,
( subgroup_member(u)
| subgroup_member(v)
| product(u,element_in_O2(u,v),v) ),
file('GRP040-3.p',unknown),
[] ).
cnf(4,axiom,
subgroup_member(b),
file('GRP040-3.p',unknown),
[] ).
cnf(5,axiom,
~ subgroup_member(d),
file('GRP040-3.p',unknown),
[] ).
cnf(6,axiom,
product(b,inverse(a),c),
file('GRP040-3.p',unknown),
[] ).
cnf(7,axiom,
product(a,c,d),
file('GRP040-3.p',unknown),
[] ).
cnf(8,axiom,
equal(inverse(inverse(u)),u),
file('GRP040-3.p',unknown),
[] ).
cnf(9,axiom,
product(identity,u,u),
file('GRP040-3.p',unknown),
[] ).
cnf(10,axiom,
product(u,identity,u),
file('GRP040-3.p',unknown),
[] ).
cnf(11,axiom,
product(inverse(u),u,identity),
file('GRP040-3.p',unknown),
[] ).
cnf(12,axiom,
product(u,inverse(u),identity),
file('GRP040-3.p',unknown),
[] ).
cnf(13,axiom,
product(u,v,multiply(u,v)),
file('GRP040-3.p',unknown),
[] ).
cnf(14,axiom,
( ~ product(u,v,w)
| ~ product(u,v,x)
| equal(x,w) ),
file('GRP040-3.p',unknown),
[] ).
cnf(15,axiom,
( ~ product(u,v,w)
| ~ product(x,v,y)
| ~ product(z,x,u)
| product(z,y,w) ),
file('GRP040-3.p',unknown),
[] ).
cnf(16,axiom,
( ~ product(u,v,w)
| ~ product(x,y,v)
| ~ product(u,x,z)
| product(z,y,w) ),
file('GRP040-3.p',unknown),
[] ).
cnf(17,axiom,
( ~ subgroup_member(u)
| ~ subgroup_member(v)
| ~ product(v,inverse(u),w)
| subgroup_member(w) ),
file('GRP040-3.p',unknown),
[] ).
cnf(22,plain,
( ~ product(a,c,u)
| equal(u,d) ),
inference(res,[status(thm),theory(equality)],[7,14]),
[iquote('0:Res:7.0,14.0')] ).
cnf(23,plain,
( ~ product(identity,u,v)
| equal(v,u) ),
inference(res,[status(thm),theory(equality)],[9,14]),
[iquote('0:Res:9.0,14.0')] ).
cnf(24,plain,
( ~ product(u,identity,v)
| equal(v,u) ),
inference(res,[status(thm),theory(equality)],[10,14]),
[iquote('0:Res:10.0,14.0')] ).
cnf(28,plain,
( ~ product(u,v,w)
| equal(w,multiply(u,v)) ),
inference(res,[status(thm),theory(equality)],[13,14]),
[iquote('0:Res:13.0,14.0')] ).
cnf(31,plain,
( ~ subgroup_member(u)
| ~ subgroup_member(identity)
| subgroup_member(inverse(u)) ),
inference(res,[status(thm),theory(equality)],[9,17]),
[iquote('0:Res:9.0,17.2')] ).
cnf(32,plain,
( ~ subgroup_member(a)
| ~ subgroup_member(b)
| subgroup_member(c) ),
inference(res,[status(thm),theory(equality)],[6,17]),
[iquote('0:Res:6.0,17.2')] ).
cnf(34,plain,
( ~ subgroup_member(u)
| ~ subgroup_member(u)
| subgroup_member(identity) ),
inference(res,[status(thm),theory(equality)],[12,17]),
[iquote('0:Res:12.0,17.2')] ).
cnf(35,plain,
( ~ subgroup_member(u)
| ~ subgroup_member(v)
| subgroup_member(multiply(v,inverse(u))) ),
inference(res,[status(thm),theory(equality)],[13,17]),
[iquote('0:Res:13.0,17.2')] ).
cnf(36,plain,
( ~ subgroup_member(a)
| subgroup_member(c) ),
inference(ssi,[status(thm)],[32,4]),
[iquote('0:SSi:32.1,4.0')] ).
cnf(37,plain,
( ~ subgroup_member(u)
| subgroup_member(identity) ),
inference(obv,[status(thm),theory(equality)],[34]),
[iquote('0:Obv:34.0')] ).
cnf(38,plain,
( ~ subgroup_member(u)
| subgroup_member(inverse(u)) ),
inference(mrr,[status(thm)],[31,37]),
[iquote('0:MRR:31.1,37.1')] ).
cnf(45,plain,
( ~ product(u,v,identity)
| ~ product(w,u,x)
| product(x,v,w) ),
inference(res,[status(thm),theory(equality)],[10,16]),
[iquote('0:Res:10.0,16.0')] ).
cnf(47,plain,
( ~ product(u,v,w)
| ~ product(inverse(w),u,x)
| product(x,v,identity) ),
inference(res,[status(thm),theory(equality)],[11,16]),
[iquote('0:Res:11.0,16.0')] ).
cnf(53,plain,
equal(multiply(a,c),d),
inference(res,[status(thm),theory(equality)],[13,22]),
[iquote('0:Res:13.0,22.0')] ).
cnf(59,plain,
equal(multiply(identity,u),u),
inference(res,[status(thm),theory(equality)],[13,23]),
[iquote('0:Res:13.0,23.0')] ).
cnf(62,plain,
( ~ product(u,v,w)
| ~ product(x,u,identity)
| product(x,w,v) ),
inference(res,[status(thm),theory(equality)],[9,15]),
[iquote('0:Res:9.0,15.0')] ).
cnf(66,plain,
( ~ product(u,inverse(v),w)
| ~ product(x,u,v)
| product(x,w,identity) ),
inference(res,[status(thm),theory(equality)],[12,15]),
[iquote('0:Res:12.0,15.0')] ).
cnf(122,plain,
( ~ subgroup_member(inverse(u))
| ~ subgroup_member(v)
| subgroup_member(multiply(v,u)) ),
inference(spr,[status(thm),theory(equality)],[8,35]),
[iquote('0:SpR:8.0,35.2')] ).
cnf(130,plain,
( ~ subgroup_member(u)
| ~ subgroup_member(v)
| subgroup_member(multiply(u,v)) ),
inference(sor,[status(thm)],[122,38]),
[iquote('0:SoR:122.0,38.1')] ).
cnf(134,plain,
( ~ subgroup_member(a)
| ~ subgroup_member(c)
| subgroup_member(d) ),
inference(spr,[status(thm),theory(equality)],[53,130]),
[iquote('0:SpR:53.0,130.2')] ).
cnf(138,plain,
~ subgroup_member(a),
inference(mrr,[status(thm)],[134,36,5]),
[iquote('0:MRR:134.1,134.2,36.1,5.0')] ).
cnf(233,plain,
( ~ product(u,inverse(v),w)
| product(w,v,u) ),
inference(res,[status(thm),theory(equality)],[11,45]),
[iquote('0:Res:11.0,45.0')] ).
cnf(245,plain,
product(c,a,b),
inference(res,[status(thm),theory(equality)],[6,233]),
[iquote('0:Res:6.0,233.0')] ).
cnf(248,plain,
product(multiply(u,inverse(v)),v,u),
inference(res,[status(thm),theory(equality)],[13,233]),
[iquote('0:Res:13.0,233.0')] ).
cnf(257,plain,
( ~ product(u,v,identity)
| product(u,identity,inverse(v)) ),
inference(res,[status(thm),theory(equality)],[12,62]),
[iquote('0:Res:12.0,62.0')] ).
cnf(263,plain,
( ~ product(u,c,identity)
| product(u,b,a) ),
inference(res,[status(thm),theory(equality)],[245,62]),
[iquote('0:Res:245.0,62.0')] ).
cnf(272,plain,
product(multiply(u,v),inverse(v),u),
inference(spr,[status(thm),theory(equality)],[8,248]),
[iquote('0:SpR:8.0,248.0')] ).
cnf(310,plain,
product(d,inverse(c),a),
inference(spr,[status(thm),theory(equality)],[53,272]),
[iquote('0:SpR:53.0,272.0')] ).
cnf(319,plain,
equal(multiply(multiply(u,v),inverse(v)),u),
inference(res,[status(thm),theory(equality)],[272,28]),
[iquote('0:Res:272.0,28.0')] ).
cnf(469,plain,
product(inverse(c),b,a),
inference(res,[status(thm),theory(equality)],[11,263]),
[iquote('0:Res:11.0,263.0')] ).
cnf(474,plain,
equal(multiply(inverse(c),b),a),
inference(res,[status(thm),theory(equality)],[469,28]),
[iquote('0:Res:469.0,28.0')] ).
cnf(480,plain,
( ~ subgroup_member(inverse(c))
| ~ subgroup_member(b)
| subgroup_member(a) ),
inference(spr,[status(thm),theory(equality)],[474,130]),
[iquote('0:SpR:474.0,130.2')] ).
cnf(484,plain,
( ~ subgroup_member(inverse(c))
| subgroup_member(a) ),
inference(ssi,[status(thm)],[480,4]),
[iquote('0:SSi:480.1,4.0')] ).
cnf(485,plain,
~ subgroup_member(inverse(c)),
inference(mrr,[status(thm)],[484,138]),
[iquote('0:MRR:484.1,138.0')] ).
cnf(494,plain,
~ subgroup_member(c),
inference(sor,[status(thm)],[485,38]),
[iquote('0:SoR:485.0,38.1')] ).
cnf(560,plain,
( ~ product(u,d,c)
| product(u,a,identity) ),
inference(res,[status(thm),theory(equality)],[310,66]),
[iquote('0:Res:310.0,66.0')] ).
cnf(693,plain,
product(multiply(c,inverse(d)),a,identity),
inference(res,[status(thm),theory(equality)],[248,560]),
[iquote('0:Res:248.0,560.0')] ).
cnf(704,plain,
equal(multiply(multiply(c,inverse(d)),a),identity),
inference(res,[status(thm),theory(equality)],[693,28]),
[iquote('0:Res:693.0,28.0')] ).
cnf(713,plain,
equal(multiply(identity,inverse(a)),multiply(c,inverse(d))),
inference(spr,[status(thm),theory(equality)],[704,319]),
[iquote('0:SpR:704.0,319.0')] ).
cnf(715,plain,
equal(multiply(c,inverse(d)),inverse(a)),
inference(rew,[status(thm),theory(equality)],[59,713]),
[iquote('0:Rew:59.0,713.0')] ).
cnf(730,plain,
product(inverse(a),d,c),
inference(spr,[status(thm),theory(equality)],[715,248]),
[iquote('0:SpR:715.0,248.0')] ).
cnf(745,plain,
( ~ product(d,u,a)
| product(c,u,identity) ),
inference(res,[status(thm),theory(equality)],[730,47]),
[iquote('0:Res:730.0,47.1')] ).
cnf(1135,plain,
( ~ product(u,v,identity)
| equal(inverse(v),u) ),
inference(res,[status(thm),theory(equality)],[257,24]),
[iquote('0:Res:257.1,24.0')] ).
cnf(1643,plain,
( ~ product(d,u,a)
| equal(inverse(u),c) ),
inference(res,[status(thm),theory(equality)],[745,1135]),
[iquote('0:Res:745.1,1135.0')] ).
cnf(1683,plain,
( subgroup_member(d)
| subgroup_member(a)
| equal(inverse(element_in_O2(d,a)),c) ),
inference(res,[status(thm),theory(equality)],[2,1643]),
[iquote('0:Res:2.2,1643.0')] ).
cnf(1686,plain,
equal(inverse(element_in_O2(d,a)),c),
inference(mrr,[status(thm)],[1683,5,138]),
[iquote('0:MRR:1683.0,1683.1,5.0,138.0')] ).
cnf(1690,plain,
( ~ subgroup_member(element_in_O2(d,a))
| subgroup_member(c) ),
inference(spr,[status(thm),theory(equality)],[1686,38]),
[iquote('0:SpR:1686.0,38.1')] ).
cnf(1719,plain,
~ subgroup_member(element_in_O2(d,a)),
inference(mrr,[status(thm)],[1690,494]),
[iquote('0:MRR:1690.1,494.0')] ).
cnf(1742,plain,
( subgroup_member(a)
| subgroup_member(d) ),
inference(sor,[status(thm)],[1719,1]),
[iquote('0:SoR:1719.0,1.2')] ).
cnf(1743,plain,
$false,
inference(mrr,[status(thm)],[1742,138,5]),
[iquote('0:MRR:1742.0,1742.1,138.0,5.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : GRP040-3 : TPTP v8.1.0. Released v1.0.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jun 14 07:07:07 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.47/0.69
% 0.47/0.69 SPASS V 3.9
% 0.47/0.69 SPASS beiseite: Proof found.
% 0.47/0.69 % SZS status Theorem
% 0.47/0.69 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.69 SPASS derived 1398 clauses, backtracked 0 clauses, performed 0 splits and kept 763 clauses.
% 0.47/0.69 SPASS allocated 76773 KBytes.
% 0.47/0.69 SPASS spent 0:00:00.35 on the problem.
% 0.47/0.69 0:00:00.04 for the input.
% 0.47/0.69 0:00:00.00 for the FLOTTER CNF translation.
% 0.47/0.69 0:00:00.02 for inferences.
% 0.47/0.69 0:00:00.00 for the backtracking.
% 0.47/0.69 0:00:00.26 for the reduction.
% 0.47/0.69
% 0.47/0.69
% 0.47/0.69 Here is a proof with depth 15, length 66 :
% 0.47/0.69 % SZS output start Refutation
% See solution above
% 0.47/0.69 Formulae used in the proof : an_element_in_O2 property_of_O2 b_is_in_subgroup d_in_subgroup b_times_a_inverse_is_c a_times_c_is_d prove_inverse_is_self_cancelling left_identity right_identity left_inverse right_inverse total_function1 total_function2 associativity1 associativity2 closure_of_product_and_inverse
% 0.47/0.69
%------------------------------------------------------------------------------