%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GEO653+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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 06:25:44 EDT 2022
% Result : Theorem 20.18s 20.38s
% Output : Refutation 20.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 32
% Syntax : Number of clauses : 110 ( 45 unt; 2 nHn; 110 RR)
% Number of literals : 208 ( 0 equ; 97 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-8 aty)
% Number of functors : 16 ( 16 usr; 16 con; 0-0 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(4,axiom,
coll(skc13,skc12,skc9),
file('GEO653+1.p',unknown),
[] ).
cnf(7,axiom,
para(skc15,skc14,skc12,skc8),
file('GEO653+1.p',unknown),
[] ).
cnf(8,axiom,
para(skc15,skc12,skc14,skc8),
file('GEO653+1.p',unknown),
[] ).
cnf(9,axiom,
para(skc15,skc8,skc9,skc11),
file('GEO653+1.p',unknown),
[] ).
cnf(10,axiom,
~ para(skc10,skc13,skc15,skc14),
file('GEO653+1.p',unknown),
[] ).
cnf(11,axiom,
( ~ coll(u,v,w)
| coll(u,w,v) ),
file('GEO653+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ para(u,v,u,w)
| coll(u,v,w) ),
file('GEO653+1.p',unknown),
[] ).
cnf(17,axiom,
( ~ para(u,v,w,x)
| para(u,v,x,w) ),
file('GEO653+1.p',unknown),
[] ).
cnf(18,axiom,
( ~ para(u,v,w,x)
| para(w,x,u,v) ),
file('GEO653+1.p',unknown),
[] ).
cnf(22,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(u,w,v,x) ),
file('GEO653+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(v,u,w,x) ),
file('GEO653+1.p',unknown),
[] ).
cnf(24,axiom,
( ~ cong(u,v,w,x)
| cong(u,v,x,w) ),
file('GEO653+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ cong(u,v,w,x)
| cong(w,x,u,v) ),
file('GEO653+1.p',unknown),
[] ).
cnf(28,axiom,
( ~ coll(u,v,w)
| ~ coll(u,v,x)
| coll(x,w,u) ),
file('GEO653+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ eqangle(u,v,w,x,y,z,w,x)
| para(u,v,y,z) ),
file('GEO653+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ para(u,v,w,x)
| eqangle(u,v,y,z,w,x,y,z) ),
file('GEO653+1.p',unknown),
[] ).
cnf(37,axiom,
( ~ cyclic(u,v,w,x)
| eqangle(w,u,w,v,x,u,x,v) ),
file('GEO653+1.p',unknown),
[] ).
cnf(38,axiom,
( ~ midp(u,v,w)
| ~ midp(x,v,y)
| para(x,u,y,w) ),
file('GEO653+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ cong(u,v,u,w)
| eqangle(u,v,v,w,v,w,u,w) ),
file('GEO653+1.p',unknown),
[] ).
cnf(41,axiom,
( ~ coll(u,v,w)
| ~ cong(u,v,u,w)
| midp(u,v,w) ),
file('GEO653+1.p',unknown),
[] ).
cnf(42,axiom,
( ~ midp(u,v,w)
| ~ perp(v,x,x,w)
| cong(v,u,x,u) ),
file('GEO653+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ para(u,v,w,x)
| ~ para(y,z,u,v)
| para(y,z,w,x) ),
file('GEO653+1.p',unknown),
[] ).
cnf(49,axiom,
( ~ cyclic(u,v,w,x)
| ~ cyclic(u,v,w,y)
| cyclic(v,w,y,x) ),
file('GEO653+1.p',unknown),
[] ).
cnf(57,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(w,x,u,v,x1,x2,y,z) ),
file('GEO653+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(y,z,x1,x2,u,v,w,x) ),
file('GEO653+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(u,v,y,z,w,x,x1,x2) ),
file('GEO653+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ eqangle(u,v,u,w,x,v,x,w)
| coll(u,x,v)
| cyclic(v,w,u,x) ),
file('GEO653+1.p',unknown),
[] ).
cnf(80,axiom,
( ~ coll(u,v,w)
| ~ midp(x,v,y)
| ~ para(x,u,y,w)
| midp(u,v,w) ),
file('GEO653+1.p',unknown),
[] ).
cnf(81,axiom,
( ~ coll(u,v,w)
| ~ eqangle(u,x,u,w,v,x,v,w)
| cyclic(x,w,u,v) ),
file('GEO653+1.p',unknown),
[] ).
cnf(90,axiom,
( ~ midp(u,v,w)
| ~ para(v,x,w,y)
| ~ para(v,y,w,x)
| midp(u,y,x) ),
file('GEO653+1.p',unknown),
[] ).
cnf(97,axiom,
( ~ cyclic(u,v,w,x)
| ~ cong(u,x,v,x)
| ~ cong(u,w,v,w)
| perp(w,u,u,x) ),
file('GEO653+1.p',unknown),
[] ).
cnf(123,axiom,
( ~ cyclic(u,v,w,x)
| ~ cyclic(u,v,w,y)
| ~ cyclic(u,v,w,z)
| ~ eqangle(w,u,w,v,z,x,z,y)
| cong(u,v,x,y) ),
file('GEO653+1.p',unknown),
[] ).
cnf(172,plain,
coll(skc13,skc9,skc12),
inference(res,[status(thm),theory(equality)],[4,11]),
[iquote('0:Res:4.0,11.0')] ).
cnf(394,plain,
para(skc9,skc11,skc15,skc8),
inference(res,[status(thm),theory(equality)],[9,18]),
[iquote('0:Res:9.0,18.0')] ).
cnf(395,plain,
para(skc14,skc8,skc15,skc12),
inference(res,[status(thm),theory(equality)],[8,18]),
[iquote('0:Res:8.0,18.0')] ).
cnf(396,plain,
para(skc12,skc8,skc15,skc14),
inference(res,[status(thm),theory(equality)],[7,18]),
[iquote('0:Res:7.0,18.0')] ).
cnf(402,plain,
para(skc15,skc12,skc8,skc14),
inference(res,[status(thm),theory(equality)],[8,17]),
[iquote('0:Res:8.0,17.0')] ).
cnf(403,plain,
para(skc15,skc14,skc8,skc12),
inference(res,[status(thm),theory(equality)],[7,17]),
[iquote('0:Res:7.0,17.0')] ).
cnf(405,plain,
para(skc14,skc8,skc12,skc15),
inference(res,[status(thm),theory(equality)],[395,17]),
[iquote('0:Res:395.0,17.0')] ).
cnf(406,plain,
para(skc12,skc8,skc14,skc15),
inference(res,[status(thm),theory(equality)],[396,17]),
[iquote('0:Res:396.0,17.0')] ).
cnf(410,plain,
para(skc8,skc14,skc15,skc12),
inference(res,[status(thm),theory(equality)],[402,18]),
[iquote('0:Res:402.0,18.0')] ).
cnf(412,plain,
para(skc8,skc12,skc15,skc14),
inference(res,[status(thm),theory(equality)],[403,18]),
[iquote('0:Res:403.0,18.0')] ).
cnf(418,plain,
para(skc14,skc15,skc12,skc8),
inference(res,[status(thm),theory(equality)],[406,18]),
[iquote('0:Res:406.0,18.0')] ).
cnf(453,plain,
( ~ coll(skc13,skc9,u)
| coll(u,skc12,skc13) ),
inference(res,[status(thm),theory(equality)],[172,28]),
[iquote('0:Res:172.0,28.0')] ).
cnf(629,plain,
( ~ cong(u,u,u,v)
| para(u,u,u,v) ),
inference(res,[status(thm),theory(equality)],[39,35]),
[iquote('0:Res:39.1,35.0')] ).
cnf(775,plain,
( ~ para(u,v,skc15,skc8)
| para(u,v,skc9,skc11) ),
inference(res,[status(thm),theory(equality)],[9,45]),
[iquote('0:Res:9.0,45.0')] ).
cnf(778,plain,
( ~ para(u,v,skc15,skc14)
| para(u,v,skc12,skc8) ),
inference(res,[status(thm),theory(equality)],[7,45]),
[iquote('0:Res:7.0,45.0')] ).
cnf(881,plain,
coll(skc12,skc12,skc13),
inference(res,[status(thm),theory(equality)],[172,453]),
[iquote('0:Res:172.0,453.0')] ).
cnf(887,plain,
coll(skc12,skc13,skc12),
inference(res,[status(thm),theory(equality)],[881,11]),
[iquote('0:Res:881.0,11.0')] ).
cnf(901,plain,
( ~ coll(skc12,skc13,u)
| coll(u,skc12,skc12) ),
inference(res,[status(thm),theory(equality)],[887,28]),
[iquote('0:Res:887.0,28.0')] ).
cnf(1046,plain,
( ~ para(u,v,w,x)
| eqangle(u,v,w,x,y,z,y,z) ),
inference(res,[status(thm),theory(equality)],[36,59]),
[iquote('0:Res:36.1,59.0')] ).
cnf(1062,plain,
( ~ cong(u,v,u,w)
| eqangle(v,w,u,w,u,v,v,w) ),
inference(res,[status(thm),theory(equality)],[39,58]),
[iquote('0:Res:39.1,58.0')] ).
cnf(1081,plain,
( ~ para(u,v,w,x)
| eqangle(y,z,u,v,y,z,w,x) ),
inference(res,[status(thm),theory(equality)],[36,57]),
[iquote('0:Res:36.1,57.0')] ).
cnf(1236,plain,
( ~ para(u,v,u,v)
| ~ coll(u,u,w)
| cyclic(v,w,u,u) ),
inference(res,[status(thm),theory(equality)],[36,81]),
[iquote('0:Res:36.1,81.1')] ).
cnf(1305,plain,
( ~ midp(u,skc8,skc15)
| ~ para(skc8,skc12,skc15,skc14)
| midp(u,skc12,skc14) ),
inference(res,[status(thm),theory(equality)],[410,90]),
[iquote('0:Res:410.0,90.1')] ).
cnf(1316,plain,
( ~ midp(u,skc14,skc12)
| ~ para(skc14,skc8,skc12,skc15)
| midp(u,skc8,skc15) ),
inference(res,[status(thm),theory(equality)],[418,90]),
[iquote('0:Res:418.0,90.1')] ).
cnf(1321,plain,
( ~ midp(u,skc8,skc15)
| midp(u,skc12,skc14) ),
inference(mrr,[status(thm)],[1305,412]),
[iquote('0:MRR:1305.1,412.0')] ).
cnf(1326,plain,
( ~ midp(u,skc14,skc12)
| midp(u,skc8,skc15) ),
inference(mrr,[status(thm)],[1316,405]),
[iquote('0:MRR:1316.1,405.0')] ).
cnf(2181,plain,
( ~ cyclic(u,v,w,x)
| ~ cyclic(u,v,w,u)
| ~ cyclic(u,v,w,v)
| ~ cyclic(u,v,w,x)
| cong(u,v,u,v) ),
inference(res,[status(thm),theory(equality)],[37,123]),
[iquote('0:Res:37.1,123.3')] ).
cnf(2183,plain,
( ~ cyclic(u,v,w,u)
| ~ cyclic(u,v,w,v)
| ~ cyclic(u,v,w,x)
| cong(u,v,u,v) ),
inference(obv,[status(thm),theory(equality)],[2181]),
[iquote('0:Obv:2181.0')] ).
cnf(2184,plain,
( ~ cyclic(u,v,w,u)
| ~ cyclic(u,v,w,v)
| cong(u,v,u,v) ),
inference(con,[status(thm)],[2183]),
[iquote('0:Con:2183.2')] ).
cnf(2489,plain,
para(skc9,skc11,skc9,skc11),
inference(res,[status(thm),theory(equality)],[394,775]),
[iquote('0:Res:394.0,775.0')] ).
cnf(2567,plain,
para(skc12,skc8,skc12,skc8),
inference(res,[status(thm),theory(equality)],[396,778]),
[iquote('0:Res:396.0,778.0')] ).
cnf(2568,plain,
para(skc8,skc12,skc12,skc8),
inference(res,[status(thm),theory(equality)],[412,778]),
[iquote('0:Res:412.0,778.0')] ).
cnf(2609,plain,
para(skc8,skc12,skc8,skc12),
inference(res,[status(thm),theory(equality)],[2568,17]),
[iquote('0:Res:2568.0,17.0')] ).
cnf(3894,plain,
coll(skc12,skc12,skc12),
inference(res,[status(thm),theory(equality)],[887,901]),
[iquote('0:Res:887.0,901.0')] ).
cnf(3908,plain,
( ~ para(u,v,u,v)
| coll(u,w,v)
| cyclic(v,v,u,w) ),
inference(res,[status(thm),theory(equality)],[1046,64]),
[iquote('0:Res:1046.1,64.0')] ).
cnf(3919,plain,
( ~ para(u,v,u,v)
| ~ coll(u,w,v)
| cyclic(v,v,u,w) ),
inference(res,[status(thm),theory(equality)],[1046,81]),
[iquote('0:Res:1046.1,81.1')] ).
cnf(3937,plain,
( ~ para(u,v,u,v)
| cyclic(v,v,u,w) ),
inference(mrr,[status(thm)],[3919,3908]),
[iquote('0:MRR:3919.1,3908.1')] ).
cnf(3995,plain,
( ~ cong(u,u,u,v)
| para(u,v,u,u) ),
inference(res,[status(thm),theory(equality)],[1062,35]),
[iquote('0:Res:1062.1,35.0')] ).
cnf(4212,plain,
( ~ para(u,v,u,v)
| para(w,x,w,x) ),
inference(res,[status(thm),theory(equality)],[1081,35]),
[iquote('0:Res:1081.1,35.0')] ).
cnf(4643,plain,
( ~ coll(skc12,skc12,u)
| cyclic(skc8,u,skc12,skc12) ),
inference(res,[status(thm),theory(equality)],[2567,1236]),
[iquote('0:Res:2567.0,1236.0')] ).
cnf(5123,plain,
( ~ midp(u,skc8,skc15)
| ~ midp(v,skc12,w)
| para(v,u,w,skc14) ),
inference(res,[status(thm),theory(equality)],[1321,38]),
[iquote('0:Res:1321.1,38.0')] ).
cnf(9625,plain,
( ~ coll(skc12,skc12,u)
| cyclic(u,skc8,skc12,skc12) ),
inference(res,[status(thm),theory(equality)],[4643,23]),
[iquote('0:Res:4643.1,23.0')] ).
cnf(9762,plain,
( ~ coll(skc12,skc12,u)
| cyclic(u,skc12,skc8,skc12) ),
inference(res,[status(thm),theory(equality)],[9625,22]),
[iquote('0:Res:9625.1,22.0')] ).
cnf(9969,plain,
( ~ coll(skc12,skc12,skc12)
| ~ cyclic(skc12,skc12,skc8,skc12)
| cong(skc12,skc12,skc12,skc12) ),
inference(res,[status(thm),theory(equality)],[9762,2184]),
[iquote('0:Res:9762.1,2184.0')] ).
cnf(9970,plain,
( ~ cyclic(skc12,skc12,skc8,skc12)
| cong(skc12,skc12,skc12,skc12) ),
inference(mrr,[status(thm)],[9969,3894]),
[iquote('0:MRR:9969.0,3894.0')] ).
cnf(17900,plain,
cyclic(skc12,skc12,skc8,u),
inference(res,[status(thm),theory(equality)],[2609,3937]),
[iquote('0:Res:2609.0,3937.0')] ).
cnf(17906,plain,
cong(skc12,skc12,skc12,skc12),
inference(mrr,[status(thm)],[9970,17900]),
[iquote('0:MRR:9970.0,17900.0')] ).
cnf(18215,plain,
( ~ coll(skc12,skc12,skc12)
| midp(skc12,skc12,skc12) ),
inference(res,[status(thm),theory(equality)],[17906,41]),
[iquote('0:Res:17906.0,41.1')] ).
cnf(18233,plain,
midp(skc12,skc12,skc12),
inference(mrr,[status(thm)],[18215,3894]),
[iquote('0:MRR:18215.0,3894.0')] ).
cnf(18251,plain,
para(u,v,u,v),
inference(res,[status(thm),theory(equality)],[2489,4212]),
[iquote('0:Res:2489.0,4212.0')] ).
cnf(18260,plain,
cyclic(u,u,v,w),
inference(mrr,[status(thm)],[3937,18251]),
[iquote('0:MRR:3937.0,18251.0')] ).
cnf(21596,plain,
( ~ cong(u,v,u,v)
| ~ cong(u,w,u,w)
| perp(w,u,u,v) ),
inference(res,[status(thm),theory(equality)],[18260,97]),
[iquote('0:Res:18260.0,97.0')] ).
cnf(21597,plain,
( ~ cyclic(u,u,v,w)
| cyclic(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[18260,49]),
[iquote('0:Res:18260.0,49.0')] ).
cnf(21654,plain,
cyclic(u,v,w,x),
inference(mrr,[status(thm)],[21597,18260]),
[iquote('0:MRR:21597.0,18260.0')] ).
cnf(21675,plain,
cong(u,v,u,v),
inference(mrr,[status(thm)],[2184,21654]),
[iquote('0:MRR:2184.1,2184.0,21654.0')] ).
cnf(21988,plain,
perp(u,v,v,w),
inference(mrr,[status(thm)],[21596,21675]),
[iquote('0:MRR:21596.0,21596.1,21675.0,21675.0')] ).
cnf(22009,plain,
( ~ midp(u,v,w)
| cong(v,u,x,u) ),
inference(mrr,[status(thm)],[42,21988]),
[iquote('0:MRR:42.1,21988.0')] ).
cnf(22676,plain,
cong(skc12,skc12,u,skc12),
inference(res,[status(thm),theory(equality)],[18233,22009]),
[iquote('0:Res:18233.0,22009.0')] ).
cnf(24004,plain,
cong(skc12,skc12,skc12,u),
inference(res,[status(thm),theory(equality)],[22676,24]),
[iquote('0:Res:22676.0,24.0')] ).
cnf(25953,plain,
cong(skc12,u,skc12,skc12),
inference(res,[status(thm),theory(equality)],[24004,25]),
[iquote('0:Res:24004.0,25.0')] ).
cnf(25956,plain,
para(skc12,u,skc12,skc12),
inference(res,[status(thm),theory(equality)],[24004,3995]),
[iquote('0:Res:24004.0,3995.0')] ).
cnf(25957,plain,
para(skc12,skc12,skc12,u),
inference(res,[status(thm),theory(equality)],[24004,629]),
[iquote('0:Res:24004.0,629.0')] ).
cnf(27237,plain,
( ~ coll(skc12,u,skc12)
| midp(skc12,u,skc12) ),
inference(res,[status(thm),theory(equality)],[25953,41]),
[iquote('0:Res:25953.0,41.1')] ).
cnf(27246,plain,
coll(skc12,u,skc12),
inference(res,[status(thm),theory(equality)],[25956,15]),
[iquote('0:Res:25956.0,15.0')] ).
cnf(27253,plain,
( ~ coll(u,v,skc12)
| ~ midp(skc12,v,skc12)
| midp(u,v,skc12) ),
inference(res,[status(thm),theory(equality)],[25956,80]),
[iquote('0:Res:25956.0,80.2')] ).
cnf(27256,plain,
( ~ midp(u,skc12,skc12)
| ~ para(skc12,skc12,skc12,v)
| midp(u,skc12,v) ),
inference(res,[status(thm),theory(equality)],[25956,90]),
[iquote('0:Res:25956.0,90.1')] ).
cnf(27266,plain,
midp(skc12,u,skc12),
inference(mrr,[status(thm)],[27237,27246]),
[iquote('0:MRR:27237.0,27246.0')] ).
cnf(27272,plain,
( ~ coll(u,v,skc12)
| midp(u,v,skc12) ),
inference(mrr,[status(thm)],[27253,27266]),
[iquote('0:MRR:27253.1,27266.0')] ).
cnf(27273,plain,
( ~ midp(u,skc12,skc12)
| midp(u,skc12,v) ),
inference(mrr,[status(thm)],[27256,25957]),
[iquote('0:MRR:27256.1,25957.0')] ).
cnf(27326,plain,
coll(skc12,skc12,u),
inference(res,[status(thm),theory(equality)],[27246,11]),
[iquote('0:Res:27246.0,11.0')] ).
cnf(27496,plain,
( ~ coll(skc12,skc12,u)
| coll(u,v,skc12) ),
inference(res,[status(thm),theory(equality)],[27326,28]),
[iquote('0:Res:27326.0,28.0')] ).
cnf(27499,plain,
coll(u,v,skc12),
inference(mrr,[status(thm)],[27496,27326]),
[iquote('0:MRR:27496.0,27326.0')] ).
cnf(27504,plain,
midp(u,v,skc12),
inference(mrr,[status(thm)],[27272,27499]),
[iquote('0:MRR:27272.0,27499.0')] ).
cnf(27522,plain,
midp(u,skc8,skc15),
inference(mrr,[status(thm)],[1326,27504]),
[iquote('0:MRR:1326.0,27504.0')] ).
cnf(27549,plain,
midp(u,skc12,v),
inference(mrr,[status(thm)],[27273,27504]),
[iquote('0:MRR:27273.0,27504.0')] ).
cnf(27610,plain,
( ~ midp(u,skc12,v)
| para(u,w,v,skc14) ),
inference(mrr,[status(thm)],[5123,27522]),
[iquote('0:MRR:5123.0,27522.0')] ).
cnf(27866,plain,
para(u,v,w,skc14),
inference(mrr,[status(thm)],[27610,27549]),
[iquote('0:MRR:27610.0,27549.0')] ).
cnf(27867,plain,
$false,
inference(unc,[status(thm)],[27866,10]),
[iquote('0:UnC:27866.0,10.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO653+1 : TPTP v8.1.0. Released v7.5.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n025.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 : Fri Jun 17 19:42:27 EDT 2022
% 0.12/0.34 % CPUTime :
% 20.18/20.38
% 20.18/20.38 SPASS V 3.9
% 20.18/20.38 SPASS beiseite: Proof found.
% 20.18/20.38 % SZS status Theorem
% 20.18/20.38 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.18/20.38 SPASS derived 26183 clauses, backtracked 0 clauses, performed 0 splits and kept 15400 clauses.
% 20.18/20.38 SPASS allocated 104006 KBytes.
% 20.18/20.38 SPASS spent 0:0:19.79 on the problem.
% 20.18/20.38 0:00:00.04 for the input.
% 20.18/20.38 0:00:00.28 for the FLOTTER CNF translation.
% 20.18/20.38 0:00:00.54 for inferences.
% 20.18/20.38 0:00:00.00 for the backtracking.
% 20.18/20.38 0:0:18.23 for the reduction.
% 20.18/20.38
% 20.18/20.38
% 20.18/20.38 Here is a proof with depth 13, length 110 :
% 20.18/20.38 % SZS output start Refutation
% See solution above
% 20.18/20.38 Formulae used in the proof : exemplo6GDDFULLmoreE0227 ruleD1 ruleD66 ruleD4 ruleD5 ruleD15 ruleD16 ruleD23 ruleD24 ruleD3 ruleD39 ruleD40 ruleD41 ruleD44 ruleD46 ruleD67 ruleD52 ruleD6 ruleD17 ruleD19 ruleD20 ruleD21 ruleD42a ruleD45 ruleD42b ruleD64 ruleD57 ruleD43
% 20.18/20.38
%------------------------------------------------------------------------------