%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : FLD008-3 : TPTP v8.1.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n028.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 02:28:14 EDT 2022
% Result : Unsatisfiable 17.14s 17.37s
% Output : Refutation 17.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of clauses : 35 ( 9 unt; 0 nHn; 35 RR)
% Number of literals : 89 ( 0 equ; 67 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
defined(a),
file('FLD008-3.p',unknown),
[] ).
cnf(2,axiom,
defined(b),
file('FLD008-3.p',unknown),
[] ).
cnf(3,axiom,
~ sum__dfg(additive_identity,additive_inverse(add(a,b)),add(additive_inverse(a),additive_inverse(b))),
file('FLD008-3.p',unknown),
[] ).
cnf(4,axiom,
( ~ sum__dfg(u,v,w)
| ~ sum__dfg(x,v,y)
| ~ sum__dfg(z,x,u)
| sum__dfg(z,y,w) ),
file('FLD008-3.p',unknown),
[] ).
cnf(5,axiom,
( ~ sum__dfg(u,v,w)
| ~ sum__dfg(x,y,v)
| ~ sum__dfg(u,x,z)
| sum__dfg(z,y,w) ),
file('FLD008-3.p',unknown),
[] ).
cnf(6,axiom,
( ~ defined(u)
| sum__dfg(additive_identity,u,u) ),
file('FLD008-3.p',unknown),
[] ).
cnf(7,axiom,
( ~ defined(u)
| sum__dfg(additive_inverse(u),u,additive_identity) ),
file('FLD008-3.p',unknown),
[] ).
cnf(8,axiom,
( ~ sum__dfg(u,v,w)
| sum__dfg(v,u,w) ),
file('FLD008-3.p',unknown),
[] ).
cnf(16,axiom,
( ~ defined(u)
| ~ defined(v)
| defined(add(v,u)) ),
file('FLD008-3.p',unknown),
[] ).
cnf(18,axiom,
( ~ defined(u)
| defined(additive_inverse(u)) ),
file('FLD008-3.p',unknown),
[] ).
cnf(22,axiom,
( ~ defined(u)
| ~ defined(v)
| sum__dfg(v,u,add(v,u)) ),
file('FLD008-3.p',unknown),
[] ).
cnf(32,plain,
( ~ sum__dfg(u,v,additive_inverse(add(a,b)))
| ~ sum__dfg(w,v,add(additive_inverse(a),additive_inverse(b)))
| ~ sum__dfg(additive_identity,u,w) ),
inference(res,[status(thm),theory(equality)],[4,3]),
[iquote('0:Res:4.3,3.0')] ).
cnf(45,plain,
( ~ defined(u)
| sum__dfg(u,additive_identity,u) ),
inference(res,[status(thm),theory(equality)],[6,8]),
[iquote('0:Res:6.1,8.0')] ).
cnf(46,plain,
( ~ defined(u)
| sum__dfg(u,additive_inverse(u),additive_identity) ),
inference(res,[status(thm),theory(equality)],[7,8]),
[iquote('0:Res:7.1,8.0')] ).
cnf(54,plain,
( ~ defined(u)
| ~ defined(v)
| sum__dfg(u,v,add(v,u)) ),
inference(res,[status(thm),theory(equality)],[22,8]),
[iquote('0:Res:22.2,8.0')] ).
cnf(121,plain,
( ~ defined(u)
| ~ sum__dfg(v,w,u)
| ~ sum__dfg(additive_inverse(u),v,x)
| sum__dfg(x,w,additive_identity) ),
inference(res,[status(thm),theory(equality)],[7,5]),
[iquote('0:Res:7.1,5.0')] ).
cnf(151,plain,
( ~ defined(u)
| ~ sum__dfg(v,u,w)
| ~ sum__dfg(x,v,additive_identity)
| sum__dfg(x,w,u) ),
inference(res,[status(thm),theory(equality)],[6,4]),
[iquote('0:Res:6.1,4.0')] ).
cnf(670,plain,
( ~ defined(u)
| ~ defined(additive_inverse(u))
| ~ sum__dfg(v,u,additive_identity)
| sum__dfg(v,additive_identity,additive_inverse(u)) ),
inference(res,[status(thm),theory(equality)],[46,151]),
[iquote('0:Res:46.1,151.1')] ).
cnf(672,plain,
( ~ defined(u)
| ~ defined(v)
| ~ defined(v)
| ~ sum__dfg(w,u,additive_identity)
| sum__dfg(w,add(v,u),v) ),
inference(res,[status(thm),theory(equality)],[54,151]),
[iquote('0:Res:54.2,151.1')] ).
cnf(676,plain,
( ~ defined(u)
| ~ sum__dfg(v,u,additive_identity)
| sum__dfg(v,additive_identity,additive_inverse(u)) ),
inference(ssi,[status(thm)],[670,18]),
[iquote('0:SSi:670.1,18.1')] ).
cnf(680,plain,
( ~ defined(u)
| ~ defined(v)
| ~ sum__dfg(w,u,additive_identity)
| sum__dfg(w,add(v,u),v) ),
inference(obv,[status(thm),theory(equality)],[672]),
[iquote('0:Obv:672.1')] ).
cnf(768,plain,
( ~ defined(u)
| ~ defined(additive_inverse(v))
| ~ defined(v)
| ~ sum__dfg(u,w,v)
| sum__dfg(add(additive_inverse(v),u),w,additive_identity) ),
inference(res,[status(thm),theory(equality)],[22,121]),
[iquote('0:Res:22.2,121.2')] ).
cnf(774,plain,
( ~ defined(u)
| ~ defined(v)
| ~ sum__dfg(u,w,v)
| sum__dfg(add(additive_inverse(v),u),w,additive_identity) ),
inference(ssi,[status(thm)],[768,18]),
[iquote('0:SSi:768.1,18.1')] ).
cnf(1042,plain,
( ~ defined(add(additive_inverse(a),additive_inverse(b)))
| ~ sum__dfg(u,additive_identity,additive_inverse(add(a,b)))
| ~ sum__dfg(additive_identity,u,add(additive_inverse(a),additive_inverse(b))) ),
inference(res,[status(thm),theory(equality)],[45,32]),
[iquote('0:Res:45.1,32.1')] ).
cnf(1053,plain,
( ~ sum__dfg(u,additive_identity,additive_inverse(add(a,b)))
| ~ sum__dfg(additive_identity,u,add(additive_inverse(a),additive_inverse(b))) ),
inference(ssi,[status(thm)],[1042,16,18,1,2]),
[iquote('0:SSi:1042.0,16.0,18.1,1.0,18.1,2.2')] ).
cnf(10715,plain,
( ~ defined(add(additive_inverse(a),additive_inverse(b)))
| ~ sum__dfg(add(additive_inverse(a),additive_inverse(b)),additive_identity,additive_inverse(add(a,b))) ),
inference(res,[status(thm),theory(equality)],[6,1053]),
[iquote('0:Res:6.1,1053.1')] ).
cnf(10726,plain,
~ sum__dfg(add(additive_inverse(a),additive_inverse(b)),additive_identity,additive_inverse(add(a,b))),
inference(ssi,[status(thm)],[10715,16,18,1,2]),
[iquote('0:SSi:10715.0,16.0,18.1,1.0,18.1,2.2')] ).
cnf(11169,plain,
( ~ defined(add(a,b))
| ~ sum__dfg(add(additive_inverse(a),additive_inverse(b)),add(a,b),additive_identity) ),
inference(res,[status(thm),theory(equality)],[676,10726]),
[iquote('0:Res:676.2,10726.0')] ).
cnf(11170,plain,
~ sum__dfg(add(additive_inverse(a),additive_inverse(b)),add(a,b),additive_identity),
inference(ssi,[status(thm)],[11169,16,1,2]),
[iquote('0:SSi:11169.0,16.0,1.0,2.2')] ).
cnf(16504,plain,
( ~ defined(additive_inverse(b))
| ~ defined(a)
| ~ sum__dfg(additive_inverse(b),add(a,b),a) ),
inference(res,[status(thm),theory(equality)],[774,11170]),
[iquote('0:Res:774.3,11170.0')] ).
cnf(16505,plain,
~ sum__dfg(additive_inverse(b),add(a,b),a),
inference(ssi,[status(thm)],[16504,1,18,2]),
[iquote('0:SSi:16504.1,16504.0,1.0,18.1,2.0')] ).
cnf(16511,plain,
( ~ defined(b)
| ~ defined(a)
| ~ sum__dfg(additive_inverse(b),b,additive_identity) ),
inference(res,[status(thm),theory(equality)],[680,16505]),
[iquote('0:Res:680.3,16505.0')] ).
cnf(16512,plain,
~ sum__dfg(additive_inverse(b),b,additive_identity),
inference(ssi,[status(thm)],[16511,1,2]),
[iquote('0:SSi:16511.1,16511.0,1.0,2.0')] ).
cnf(16513,plain,
~ defined(b),
inference(res,[status(thm),theory(equality)],[7,16512]),
[iquote('0:Res:7.1,16512.0')] ).
cnf(16516,plain,
$false,
inference(ssi,[status(thm)],[16513,2]),
[iquote('0:SSi:16513.0,2.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : FLD008-3 : TPTP v8.1.0. Bugfixed v2.1.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n028.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 6 17:27:29 EDT 2022
% 0.13/0.35 % CPUTime :
% 17.14/17.37
% 17.14/17.37 SPASS V 3.9
% 17.14/17.37 SPASS beiseite: Proof found.
% 17.14/17.37 % SZS status Theorem
% 17.14/17.37 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.14/17.37 SPASS derived 12089 clauses, backtracked 344 clauses, performed 6 splits and kept 6835 clauses.
% 17.14/17.37 SPASS allocated 88611 KBytes.
% 17.14/17.37 SPASS spent 0:0:16.35 on the problem.
% 17.14/17.37 0:00:00.03 for the input.
% 17.14/17.37 0:00:00.00 for the FLOTTER CNF translation.
% 17.14/17.37 0:00:00.13 for inferences.
% 17.14/17.37 0:00:00.31 for the backtracking.
% 17.14/17.37 0:0:15.76 for the reduction.
% 17.14/17.37
% 17.14/17.37
% 17.14/17.37 Here is a proof with depth 7, length 35 :
% 17.14/17.37 % SZS output start Refutation
% See solution above
% 17.14/17.37 Formulae used in the proof : a_is_defined b_is_defined not_sum_3 associativity_addition_1 associativity_addition_2 existence_of_identity_addition existence_of_inverse_addition commutativity_addition well_definedness_of_addition well_definedness_of_additive_inverse totality_of_addition
% 17.14/17.37
%------------------------------------------------------------------------------