%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GEO548+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n018.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:10 EDT 2022
% Result : Theorem 35.47s 35.67s
% Output : Refutation 35.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 34
% Syntax : Number of clauses : 139 ( 41 unt; 5 nHn; 139 RR)
% Number of literals : 301 ( 0 equ; 158 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 21 ( 21 usr; 21 con; 0-0 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
coll(skc17,skc19,skc18),
file('GEO548+1.p',unknown),
[] ).
cnf(9,axiom,
perp(skc13,skc23,skc19,skc18),
file('GEO548+1.p',unknown),
[] ).
cnf(11,axiom,
perp(skc17,skc22,skc19,skc18),
file('GEO548+1.p',unknown),
[] ).
cnf(14,axiom,
( ~ coll(u,v,w)
| coll(u,w,v) ),
file('GEO548+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ coll(u,v,w)
| coll(v,u,w) ),
file('GEO548+1.p',unknown),
[] ).
cnf(18,axiom,
~ eqangle(skc22,skc19,skc19,skc23,skc14,skc15,skc15,skc16),
file('GEO548+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ para(u,v,u,w)
| coll(u,v,w) ),
file('GEO548+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ midp(u,v,w)
| cong(u,v,u,w) ),
file('GEO548+1.p',unknown),
[] ).
cnf(22,axiom,
( ~ para(u,v,w,x)
| para(w,x,u,v) ),
file('GEO548+1.p',unknown),
[] ).
cnf(24,axiom,
( ~ perp(u,v,w,x)
| perp(w,x,u,v) ),
file('GEO548+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(u,v,x,w) ),
file('GEO548+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(u,w,v,x) ),
file('GEO548+1.p',unknown),
[] ).
cnf(27,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(v,u,w,x) ),
file('GEO548+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ coll(u,v,w)
| ~ coll(u,v,x)
| coll(x,w,u) ),
file('GEO548+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ eqangle(u,v,w,x,y,z,w,x)
| para(u,v,y,z) ),
file('GEO548+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ para(u,v,w,x)
| eqangle(u,v,y,z,w,x,y,z) ),
file('GEO548+1.p',unknown),
[] ).
cnf(41,axiom,
( ~ cyclic(u,v,w,x)
| eqangle(w,u,w,v,x,u,x,v) ),
file('GEO548+1.p',unknown),
[] ).
cnf(43,axiom,
( ~ cong(u,v,u,w)
| eqangle(u,v,v,w,v,w,u,w) ),
file('GEO548+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ coll(u,v,w)
| ~ cong(u,v,u,w)
| midp(u,v,w) ),
file('GEO548+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ perp(u,v,w,x)
| ~ perp(y,z,u,v)
| para(y,z,w,x) ),
file('GEO548+1.p',unknown),
[] ).
cnf(52,axiom,
( ~ cong(u,v,u,w)
| ~ cong(u,v,u,x)
| circle(u,v,x,w) ),
file('GEO548+1.p',unknown),
[] ).
cnf(53,axiom,
( ~ cyclic(u,v,w,x)
| ~ cyclic(u,v,w,y)
| cyclic(v,w,y,x) ),
file('GEO548+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ cong(u,v,w,v)
| ~ cong(u,x,w,x)
| perp(u,w,x,v) ),
file('GEO548+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(w,x,u,v,x1,x2,y,z) ),
file('GEO548+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(y,z,x1,x2,u,v,w,x) ),
file('GEO548+1.p',unknown),
[] ).
cnf(63,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(u,v,y,z,w,x,x1,x2) ),
file('GEO548+1.p',unknown),
[] ).
cnf(68,axiom,
( ~ eqangle(u,v,u,w,x,v,x,w)
| coll(u,x,v)
| cyclic(v,w,u,x) ),
file('GEO548+1.p',unknown),
[] ).
cnf(83,axiom,
( ~ midp(u,v,w)
| ~ circle(x,y,v,w)
| eqangle(y,v,y,w,x,v,x,u) ),
file('GEO548+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ coll(u,v,w)
| ~ eqangle(u,x,u,w,v,x,v,w)
| cyclic(x,w,u,v) ),
file('GEO548+1.p',unknown),
[] ).
cnf(94,axiom,
( ~ midp(u,v,w)
| ~ para(v,x,w,y)
| ~ para(v,y,w,x)
| midp(u,y,x) ),
file('GEO548+1.p',unknown),
[] ).
cnf(96,axiom,
( ~ para(u,v,w,x)
| ~ cyclic(u,v,w,x)
| eqangle(u,x,w,x,w,x,w,v) ),
file('GEO548+1.p',unknown),
[] ).
cnf(113,axiom,
( ~ coll(u,v,w)
| ~ circle(x,y,v,w)
| ~ eqangle(y,v,y,w,x,v,x,u)
| midp(u,v,w) ),
file('GEO548+1.p',unknown),
[] ).
cnf(121,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| ~ eqangle(x3,x4,x5,x6,u,v,w,x)
| eqangle(x3,x4,x5,x6,y,z,x1,x2) ),
file('GEO548+1.p',unknown),
[] ).
cnf(127,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('GEO548+1.p',unknown),
[] ).
cnf(198,plain,
( ~ coll(skc17,skc19,u)
| coll(skc18,u,skc17) ),
inference(res,[status(thm),theory(equality)],[3,32]),
[iquote('0:Res:3.0,32.0')] ).
cnf(199,plain,
coll(skc17,skc18,skc19),
inference(res,[status(thm),theory(equality)],[3,14]),
[iquote('0:Res:3.0,14.0')] ).
cnf(326,plain,
( ~ coll(skc17,skc19,u)
| coll(skc18,skc17,u) ),
inference(res,[status(thm),theory(equality)],[198,14]),
[iquote('0:Res:198.1,14.0')] ).
cnf(401,plain,
perp(skc19,skc18,skc17,skc22),
inference(res,[status(thm),theory(equality)],[11,24]),
[iquote('0:Res:11.0,24.0')] ).
cnf(403,plain,
perp(skc19,skc18,skc13,skc23),
inference(res,[status(thm),theory(equality)],[9,24]),
[iquote('0:Res:9.0,24.0')] ).
cnf(485,plain,
( ~ coll(skc17,skc18,u)
| coll(u,skc19,skc17) ),
inference(res,[status(thm),theory(equality)],[199,32]),
[iquote('0:Res:199.0,32.0')] ).
cnf(558,plain,
( ~ coll(skc17,skc19,u)
| ~ coll(skc18,skc17,v)
| coll(v,u,skc18) ),
inference(res,[status(thm),theory(equality)],[326,32]),
[iquote('0:Res:326.1,32.0')] ).
cnf(668,plain,
( ~ cong(u,u,u,v)
| para(u,u,u,v) ),
inference(res,[status(thm),theory(equality)],[43,39]),
[iquote('0:Res:43.1,39.0')] ).
cnf(761,plain,
( ~ midp(u,v,w)
| ~ cong(u,v,u,x)
| circle(u,v,x,w) ),
inference(res,[status(thm),theory(equality)],[20,52]),
[iquote('0:Res:20.1,52.0')] ).
cnf(776,plain,
( ~ midp(u,v,v)
| ~ cong(u,w,u,w)
| perp(u,u,w,v) ),
inference(res,[status(thm),theory(equality)],[20,55]),
[iquote('0:Res:20.1,55.0')] ).
cnf(877,plain,
( ~ perp(u,v,skc13,skc23)
| para(u,v,skc19,skc18) ),
inference(res,[status(thm),theory(equality)],[9,50]),
[iquote('0:Res:9.0,50.0')] ).
cnf(883,plain,
( ~ perp(u,v,skc19,skc18)
| para(u,v,skc17,skc22) ),
inference(res,[status(thm),theory(equality)],[401,50]),
[iquote('0:Res:401.0,50.0')] ).
cnf(1175,plain,
( ~ para(u,v,u,v)
| coll(u,u,v)
| cyclic(v,w,u,u) ),
inference(res,[status(thm),theory(equality)],[40,68]),
[iquote('0:Res:40.1,68.0')] ).
cnf(1221,plain,
coll(skc19,skc19,skc17),
inference(res,[status(thm),theory(equality)],[199,485]),
[iquote('0:Res:199.0,485.0')] ).
cnf(1225,plain,
( ~ coll(skc19,skc19,u)
| coll(u,skc17,skc19) ),
inference(res,[status(thm),theory(equality)],[1221,32]),
[iquote('0:Res:1221.0,32.0')] ).
cnf(1252,plain,
( ~ para(u,v,w,x)
| eqangle(u,v,w,x,y,z,y,z) ),
inference(res,[status(thm),theory(equality)],[40,63]),
[iquote('0:Res:40.1,63.0')] ).
cnf(1254,plain,
( ~ cyclic(u,v,w,x)
| eqangle(w,u,x,u,w,v,x,v) ),
inference(res,[status(thm),theory(equality)],[41,63]),
[iquote('0:Res:41.1,63.0')] ).
cnf(1299,plain,
( ~ cong(u,v,u,w)
| eqangle(v,w,u,v,u,w,v,w) ),
inference(res,[status(thm),theory(equality)],[43,61]),
[iquote('0:Res:43.1,61.0')] ).
cnf(1300,plain,
( ~ para(u,v,w,x)
| eqangle(y,z,u,v,y,z,w,x) ),
inference(res,[status(thm),theory(equality)],[40,61]),
[iquote('0:Res:40.1,61.0')] ).
cnf(1624,plain,
( ~ para(u,v,u,v)
| ~ coll(u,u,w)
| cyclic(v,w,u,u) ),
inference(res,[status(thm),theory(equality)],[40,85]),
[iquote('0:Res:40.1,85.1')] ).
cnf(1673,plain,
( ~ midp(u,v,w)
| ~ circle(x,y,v,w)
| eqangle(y,v,x,v,y,w,x,u) ),
inference(res,[status(thm),theory(equality)],[83,63]),
[iquote('0:Res:83.2,63.0')] ).
cnf(1818,plain,
( ~ para(u,v,w,x)
| ~ cyclic(u,v,w,x)
| eqangle(w,x,w,v,u,x,w,x) ),
inference(res,[status(thm),theory(equality)],[96,62]),
[iquote('0:Res:96.2,62.0')] ).
cnf(2296,plain,
( ~ midp(u,v,w)
| ~ circle(x,y,v,w)
| ~ eqangle(z,x1,x2,x3,y,v,y,w)
| eqangle(z,x1,x2,x3,x,v,x,u) ),
inference(res,[status(thm),theory(equality)],[83,121]),
[iquote('0:Res:83.2,121.0')] ).
cnf(2363,plain,
( ~ para(u,v,u,w)
| ~ cyclic(u,v,u,w)
| ~ cyclic(w,w,u,w)
| ~ cyclic(w,w,u,v)
| ~ cyclic(w,w,u,u)
| cong(w,w,w,v) ),
inference(res,[status(thm),theory(equality)],[96,127]),
[iquote('0:Res:96.2,127.3')] ).
cnf(2364,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)],[41,127]),
[iquote('0:Res:41.1,127.3')] ).
cnf(2366,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)],[2364]),
[iquote('0:Obv:2364.0')] ).
cnf(2367,plain,
( ~ cyclic(u,v,w,u)
| ~ cyclic(u,v,w,v)
| cong(u,v,u,v) ),
inference(con,[status(thm)],[2366]),
[iquote('0:Con:2366.2')] ).
cnf(3044,plain,
( ~ midp(u,u,v)
| para(u,u,u,v) ),
inference(res,[status(thm),theory(equality)],[20,668]),
[iquote('0:Res:20.1,668.0')] ).
cnf(4155,plain,
( ~ para(u,v,u,v)
| coll(u,w,v)
| cyclic(v,v,u,w) ),
inference(res,[status(thm),theory(equality)],[1252,68]),
[iquote('0:Res:1252.1,68.0')] ).
cnf(4166,plain,
( ~ para(u,v,u,v)
| ~ coll(u,w,v)
| cyclic(v,v,u,w) ),
inference(res,[status(thm),theory(equality)],[1252,85]),
[iquote('0:Res:1252.1,85.1')] ).
cnf(4184,plain,
( ~ para(u,v,u,v)
| cyclic(v,v,u,w) ),
inference(mrr,[status(thm)],[4166,4155]),
[iquote('0:MRR:4166.1,4155.1')] ).
cnf(4228,plain,
( ~ cyclic(u,v,w,w)
| ~ cyclic(u,u,w,v)
| ~ cyclic(u,u,w,v)
| ~ cyclic(u,u,w,w)
| cong(u,u,v,v) ),
inference(res,[status(thm),theory(equality)],[1254,127]),
[iquote('0:Res:1254.1,127.3')] ).
cnf(4239,plain,
( ~ cyclic(u,v,w,w)
| ~ cyclic(u,u,w,v)
| ~ cyclic(u,u,w,w)
| cong(u,u,v,v) ),
inference(obv,[status(thm),theory(equality)],[4228]),
[iquote('0:Obv:4228.1')] ).
cnf(4423,plain,
( ~ cong(u,u,u,v)
| ~ coll(v,v,u)
| ~ circle(u,u,v,u)
| midp(v,v,u) ),
inference(res,[status(thm),theory(equality)],[1299,113]),
[iquote('0:Res:1299.1,113.2')] ).
cnf(4462,plain,
( ~ para(u,v,u,v)
| para(w,x,w,x) ),
inference(res,[status(thm),theory(equality)],[1300,39]),
[iquote('0:Res:1300.1,39.0')] ).
cnf(4675,plain,
( ~ midp(u,v,w)
| ~ midp(u,v,x)
| circle(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[20,761]),
[iquote('0:Res:20.1,761.1')] ).
cnf(4699,plain,
( ~ midp(u,v,v)
| ~ midp(u,w,w)
| perp(u,u,v,w) ),
inference(res,[status(thm),theory(equality)],[20,776]),
[iquote('0:Res:20.1,776.1')] ).
cnf(4741,plain,
( ~ perp(skc19,skc18,skc13,skc23)
| ~ coll(skc19,skc19,u)
| cyclic(skc18,u,skc19,skc19) ),
inference(res,[status(thm),theory(equality)],[877,1624]),
[iquote('0:Res:877.1,1624.0')] ).
cnf(4745,plain,
( ~ coll(skc19,skc19,u)
| cyclic(skc18,u,skc19,skc19) ),
inference(mrr,[status(thm)],[4741,403]),
[iquote('0:MRR:4741.0,403.0')] ).
cnf(7552,plain,
( ~ midp(u,v,w)
| ~ circle(x,y,v,w)
| ~ eqangle(z,x1,x2,x3,y,v,x,v)
| eqangle(z,x1,x2,x3,y,w,x,u) ),
inference(res,[status(thm),theory(equality)],[1673,121]),
[iquote('0:Res:1673.2,121.0')] ).
cnf(8797,plain,
( ~ para(u,v,w,x)
| ~ cyclic(u,v,w,x)
| ~ eqangle(y,z,x1,x2,w,x,w,v)
| eqangle(y,z,x1,x2,u,x,w,x) ),
inference(res,[status(thm),theory(equality)],[1818,121]),
[iquote('0:Res:1818.2,121.0')] ).
cnf(15154,plain,
( ~ para(u,v,w,x)
| ~ midp(y,z,z)
| ~ circle(x1,x2,z,z)
| eqangle(u,v,w,x,x1,z,x1,y) ),
inference(res,[status(thm),theory(equality)],[1252,2296]),
[iquote('0:Res:1252.1,2296.2')] ).
cnf(15742,plain,
( ~ coll(skc19,skc19,u)
| cyclic(skc18,skc19,u,skc19) ),
inference(res,[status(thm),theory(equality)],[4745,26]),
[iquote('0:Res:4745.1,26.0')] ).
cnf(15908,plain,
( ~ midp(u,u,v)
| para(u,v,u,u) ),
inference(res,[status(thm),theory(equality)],[3044,22]),
[iquote('0:Res:3044.1,22.0')] ).
cnf(15923,plain,
( ~ midp(u,u,v)
| ~ midp(w,u,u)
| ~ para(u,v,u,u)
| midp(w,v,u) ),
inference(res,[status(thm),theory(equality)],[3044,94]),
[iquote('0:Res:3044.1,94.1')] ).
cnf(15964,plain,
( ~ midp(u,u,v)
| ~ midp(w,u,u)
| midp(w,v,u) ),
inference(mrr,[status(thm)],[15923,15908]),
[iquote('0:MRR:15923.2,15908.1')] ).
cnf(18061,plain,
( ~ perp(skc17,skc22,skc19,skc18)
| para(u,v,u,v) ),
inference(res,[status(thm),theory(equality)],[883,4462]),
[iquote('0:Res:883.1,4462.0')] ).
cnf(30333,plain,
para(u,v,u,v),
inference(mrr,[status(thm)],[18061,11]),
[iquote('0:MRR:18061.0,11.0')] ).
cnf(30334,plain,
cyclic(u,u,v,w),
inference(mrr,[status(thm)],[4184,30333]),
[iquote('0:MRR:4184.0,30333.0')] ).
cnf(30335,plain,
( coll(u,u,v)
| cyclic(v,w,u,u) ),
inference(mrr,[status(thm)],[1175,30333]),
[iquote('0:MRR:1175.0,30333.0')] ).
cnf(30339,plain,
( ~ coll(u,u,v)
| cyclic(w,v,u,u) ),
inference(mrr,[status(thm)],[1624,30333]),
[iquote('0:MRR:1624.0,30333.0')] ).
cnf(30356,plain,
( ~ cyclic(u,v,w,w)
| cong(u,u,v,v) ),
inference(mrr,[status(thm)],[4239,30334]),
[iquote('0:MRR:4239.1,4239.2,30334.0,30334.0')] ).
cnf(30502,plain,
( ~ para(u,v,u,w)
| ~ cyclic(u,v,u,w)
| cong(w,w,w,v) ),
inference(mrr,[status(thm)],[2363,30334]),
[iquote('0:MRR:2363.2,2363.3,2363.4,30334.0,30334.0,30334.0')] ).
cnf(32504,plain,
( coll(u,u,v)
| cyclic(w,v,u,u) ),
inference(res,[status(thm),theory(equality)],[30335,27]),
[iquote('0:Res:30335.1,27.0')] ).
cnf(32507,plain,
cyclic(u,v,w,w),
inference(mrr,[status(thm)],[32504,30339]),
[iquote('0:MRR:32504.0,30339.0')] ).
cnf(32510,plain,
cong(u,u,v,v),
inference(mrr,[status(thm)],[30356,32507]),
[iquote('0:MRR:30356.0,32507.0')] ).
cnf(33869,plain,
coll(u,v,v),
inference(res,[status(thm),theory(equality)],[30333,19]),
[iquote('0:Res:30333.0,19.0')] ).
cnf(33878,plain,
( ~ midp(u,v,v)
| ~ para(v,w,v,w)
| midp(u,w,w) ),
inference(res,[status(thm),theory(equality)],[30333,94]),
[iquote('0:Res:30333.0,94.1')] ).
cnf(33927,plain,
( ~ midp(u,v,v)
| midp(u,w,w) ),
inference(mrr,[status(thm)],[33878,30333]),
[iquote('0:MRR:33878.1,30333.0')] ).
cnf(33928,plain,
( ~ midp(u,v,v)
| perp(u,u,w,v) ),
inference(mrr,[status(thm)],[4699,33927]),
[iquote('0:MRR:4699.0,33927.1')] ).
cnf(33935,plain,
coll(u,v,u),
inference(res,[status(thm),theory(equality)],[33869,15]),
[iquote('0:Res:33869.0,15.0')] ).
cnf(33953,plain,
coll(u,u,v),
inference(res,[status(thm),theory(equality)],[33935,14]),
[iquote('0:Res:33935.0,14.0')] ).
cnf(34013,plain,
coll(u,skc17,skc19),
inference(mrr,[status(thm)],[1225,33953]),
[iquote('0:MRR:1225.0,33953.0')] ).
cnf(34020,plain,
cyclic(skc18,skc19,u,skc19),
inference(mrr,[status(thm)],[15742,33953]),
[iquote('0:MRR:15742.0,33953.0')] ).
cnf(34121,plain,
( ~ cong(u,u,u,v)
| ~ circle(u,u,v,u)
| midp(v,v,u) ),
inference(mrr,[status(thm)],[4423,33953]),
[iquote('0:MRR:4423.1,33953.0')] ).
cnf(34397,plain,
coll(skc17,u,skc19),
inference(res,[status(thm),theory(equality)],[34013,15]),
[iquote('0:Res:34013.0,15.0')] ).
cnf(34818,plain,
coll(skc17,skc19,u),
inference(res,[status(thm),theory(equality)],[34397,14]),
[iquote('0:Res:34397.0,14.0')] ).
cnf(34820,plain,
coll(skc18,skc17,u),
inference(mrr,[status(thm)],[326,34818]),
[iquote('0:MRR:326.0,34818.0')] ).
cnf(34821,plain,
( ~ coll(skc18,skc17,u)
| coll(u,v,skc18) ),
inference(mrr,[status(thm)],[558,34818]),
[iquote('0:MRR:558.0,34818.0')] ).
cnf(34824,plain,
coll(u,v,skc18),
inference(mrr,[status(thm)],[34821,34820]),
[iquote('0:MRR:34821.0,34820.0')] ).
cnf(35311,plain,
coll(u,skc18,v),
inference(res,[status(thm),theory(equality)],[34824,14]),
[iquote('0:Res:34824.0,14.0')] ).
cnf(35659,plain,
( ~ coll(u,skc18,v)
| coll(v,w,u) ),
inference(res,[status(thm),theory(equality)],[35311,32]),
[iquote('0:Res:35311.0,32.0')] ).
cnf(35670,plain,
coll(u,v,w),
inference(mrr,[status(thm)],[35659,35311]),
[iquote('0:MRR:35659.0,35311.0')] ).
cnf(35671,plain,
( ~ cong(u,v,u,w)
| midp(u,v,w) ),
inference(mrr,[status(thm)],[45,35670]),
[iquote('0:MRR:45.0,35670.0')] ).
cnf(36066,plain,
cyclic(skc18,skc19,skc19,u),
inference(res,[status(thm),theory(equality)],[34020,25]),
[iquote('0:Res:34020.0,25.0')] ).
cnf(36078,plain,
cyclic(skc19,skc18,skc19,u),
inference(res,[status(thm),theory(equality)],[36066,27]),
[iquote('0:Res:36066.0,27.0')] ).
cnf(36109,plain,
( ~ cyclic(skc19,skc18,skc19,u)
| cyclic(skc18,skc19,u,v) ),
inference(res,[status(thm),theory(equality)],[36078,53]),
[iquote('0:Res:36078.0,53.0')] ).
cnf(36113,plain,
cyclic(skc18,skc19,u,v),
inference(mrr,[status(thm)],[36109,36078]),
[iquote('0:MRR:36109.0,36078.0')] ).
cnf(36129,plain,
( ~ cyclic(skc18,skc19,u,v)
| cyclic(skc19,u,v,w) ),
inference(res,[status(thm),theory(equality)],[36113,53]),
[iquote('0:Res:36113.0,53.0')] ).
cnf(36150,plain,
cyclic(skc19,u,v,w),
inference(mrr,[status(thm)],[36129,36113]),
[iquote('0:MRR:36129.0,36113.0')] ).
cnf(36319,plain,
( ~ cyclic(skc19,u,v,w)
| cyclic(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[36150,53]),
[iquote('0:Res:36150.0,53.0')] ).
cnf(36323,plain,
cyclic(u,v,w,x),
inference(mrr,[status(thm)],[36319,36150]),
[iquote('0:MRR:36319.0,36150.0')] ).
cnf(36404,plain,
( ~ para(u,v,w,x)
| ~ eqangle(y,z,x1,x2,w,x,w,v)
| eqangle(y,z,x1,x2,u,x,w,x) ),
inference(mrr,[status(thm)],[8797,36323]),
[iquote('0:MRR:8797.1,36323.0')] ).
cnf(36415,plain,
cong(u,v,u,v),
inference(mrr,[status(thm)],[2367,36323]),
[iquote('0:MRR:2367.1,2367.0,36323.0')] ).
cnf(36431,plain,
( ~ para(u,v,u,w)
| cong(w,w,w,v) ),
inference(mrr,[status(thm)],[30502,36323]),
[iquote('0:MRR:30502.1,36323.0')] ).
cnf(36559,plain,
( ~ cong(u,u,u,v)
| circle(u,u,v,u) ),
inference(res,[status(thm),theory(equality)],[32510,52]),
[iquote('0:Res:32510.0,52.0')] ).
cnf(36565,plain,
( ~ cong(u,u,u,v)
| midp(v,v,u) ),
inference(mrr,[status(thm)],[34121,36559]),
[iquote('0:MRR:34121.1,36559.1')] ).
cnf(36573,plain,
midp(u,v,v),
inference(res,[status(thm),theory(equality)],[36415,35671]),
[iquote('0:Res:36415.0,35671.0')] ).
cnf(36584,plain,
perp(u,u,v,w),
inference(mrr,[status(thm)],[33928,36573]),
[iquote('0:MRR:33928.0,36573.0')] ).
cnf(36588,plain,
( ~ midp(u,u,v)
| midp(w,v,u) ),
inference(mrr,[status(thm)],[15964,36573]),
[iquote('0:MRR:15964.1,36573.0')] ).
cnf(36591,plain,
( ~ para(u,v,w,x)
| ~ circle(y,z,x1,x1)
| eqangle(u,v,w,x,y,x1,y,x2) ),
inference(mrr,[status(thm)],[15154,36573]),
[iquote('0:MRR:15154.1,36573.0')] ).
cnf(36649,plain,
( ~ perp(u,v,w,w)
| para(u,v,x,y) ),
inference(res,[status(thm),theory(equality)],[36584,50]),
[iquote('0:Res:36584.0,50.0')] ).
cnf(36651,plain,
perp(u,v,w,w),
inference(res,[status(thm),theory(equality)],[36584,24]),
[iquote('0:Res:36584.0,24.0')] ).
cnf(36707,plain,
para(u,v,w,x),
inference(mrr,[status(thm)],[36649,36651]),
[iquote('0:MRR:36649.0,36651.0')] ).
cnf(36722,plain,
cong(u,u,u,v),
inference(mrr,[status(thm)],[36431,36707]),
[iquote('0:MRR:36431.0,36707.0')] ).
cnf(36889,plain,
( ~ eqangle(u,v,w,x,y,z,y,x1)
| eqangle(u,v,w,x,x2,z,y,z) ),
inference(mrr,[status(thm)],[36404,36707]),
[iquote('0:MRR:36404.0,36707.0')] ).
cnf(36896,plain,
( ~ circle(u,v,w,w)
| eqangle(x,y,z,x1,u,w,u,x2) ),
inference(mrr,[status(thm)],[36591,36707]),
[iquote('0:MRR:36591.0,36707.0')] ).
cnf(37077,plain,
midp(u,u,v),
inference(mrr,[status(thm)],[36565,36722]),
[iquote('0:MRR:36565.0,36722.0')] ).
cnf(37103,plain,
midp(u,v,w),
inference(mrr,[status(thm)],[36588,37077]),
[iquote('0:MRR:36588.0,37077.0')] ).
cnf(37780,plain,
circle(u,v,w,x),
inference(mrr,[status(thm)],[4675,37103]),
[iquote('0:MRR:4675.1,4675.0,37103.0')] ).
cnf(37869,plain,
( ~ circle(u,v,w,x)
| ~ eqangle(y,z,x1,x2,v,w,u,w)
| eqangle(y,z,x1,x2,v,x,u,x3) ),
inference(mrr,[status(thm)],[7552,37103]),
[iquote('0:MRR:7552.0,37103.0')] ).
cnf(38736,plain,
eqangle(u,v,w,x,y,z,y,x1),
inference(mrr,[status(thm)],[36896,37780]),
[iquote('0:MRR:36896.0,37780.0')] ).
cnf(38743,plain,
eqangle(u,v,w,x,y,z,x1,z),
inference(mrr,[status(thm)],[36889,38736]),
[iquote('0:MRR:36889.0,38736.0')] ).
cnf(38749,plain,
eqangle(u,v,w,x,y,z,x1,x2),
inference(mrr,[status(thm)],[37869,37780,38743]),
[iquote('0:MRR:37869.0,37869.1,37780.0,38743.0')] ).
cnf(38750,plain,
$false,
inference(unc,[status(thm)],[38749,18]),
[iquote('0:UnC:38749.0,18.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO548+1 : TPTP v8.1.0. Released v7.5.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n018.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Sat Jun 18 02:08:32 EDT 2022
% 0.13/0.35 % CPUTime :
% 35.47/35.67
% 35.47/35.67 SPASS V 3.9
% 35.47/35.67 SPASS beiseite: Proof found.
% 35.47/35.67 % SZS status Theorem
% 35.47/35.67 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.47/35.67 SPASS derived 37959 clauses, backtracked 9542 clauses, performed 1 splits and kept 26962 clauses.
% 35.47/35.67 SPASS allocated 112539 KBytes.
% 35.47/35.67 SPASS spent 0:0:35.26 on the problem.
% 35.47/35.67 0:00:00.04 for the input.
% 35.47/35.67 0:00:00.22 for the FLOTTER CNF translation.
% 35.47/35.67 0:00:00.50 for inferences.
% 35.47/35.67 0:00:00.03 for the backtracking.
% 35.47/35.67 0:0:33.49 for the reduction.
% 35.47/35.67
% 35.47/35.67
% 35.47/35.67 Here is a proof with depth 8, length 139 :
% 35.47/35.67 % SZS output start Refutation
% See solution above
% 35.60/35.78 Formulae used in the proof : exemplo6GDDFULL012008 ruleD1 ruleD2 ruleD66 ruleD68 ruleD5 ruleD8 ruleD14 ruleD15 ruleD16 ruleD3 ruleD39 ruleD40 ruleD41 ruleD46 ruleD67 ruleD9 ruleD12 ruleD17 ruleD56 ruleD19 ruleD20 ruleD21 ruleD42a ruleD50 ruleD42b ruleD64 ruleD54 ruleD51 ruleD22 ruleD43
% 35.60/35.78
%------------------------------------------------------------------------------