%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GEO645+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n022.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:41 EDT 2022
% Result : Theorem 14.40s 14.61s
% Output : Refutation 14.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 42
% Syntax : Number of clauses : 204 ( 86 unt; 4 nHn; 204 RR)
% Number of literals : 384 ( 0 equ; 177 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 16 ( 16 usr; 15 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
coll(skc11,skc13,skc9),
file('GEO645+1.p',unknown),
[] ).
cnf(2,axiom,
coll(skc12,skc13,skc10),
file('GEO645+1.p',unknown),
[] ).
cnf(5,axiom,
perp(skc14,skc10,skc10,skc13),
file('GEO645+1.p',unknown),
[] ).
cnf(6,axiom,
perp(skc14,skc9,skc9,skc13),
file('GEO645+1.p',unknown),
[] ).
cnf(7,axiom,
circle(skc14,skc13,skc11,skc17),
file('GEO645+1.p',unknown),
[] ).
cnf(8,axiom,
~ para(skc9,skc10,skc11,skc12),
file('GEO645+1.p',unknown),
[] ).
cnf(9,axiom,
( ~ coll(u,v,w)
| coll(u,w,v) ),
file('GEO645+1.p',unknown),
[] ).
cnf(10,axiom,
( ~ coll(u,v,w)
| coll(v,u,w) ),
file('GEO645+1.p',unknown),
[] ).
cnf(11,axiom,
( ~ midp(u,v,w)
| midp(u,w,v) ),
file('GEO645+1.p',unknown),
[] ).
cnf(13,axiom,
( ~ para(u,v,u,w)
| coll(u,v,w) ),
file('GEO645+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ para(u,v,w,x)
| para(u,v,x,w) ),
file('GEO645+1.p',unknown),
[] ).
cnf(16,axiom,
( ~ para(u,v,w,x)
| para(w,x,u,v) ),
file('GEO645+1.p',unknown),
[] ).
cnf(18,axiom,
( ~ perp(u,v,w,x)
| perp(w,x,u,v) ),
file('GEO645+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(u,v,x,w) ),
file('GEO645+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(u,w,v,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(v,u,w,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ coll(u,v,w)
| ~ coll(u,v,x)
| coll(x,w,u) ),
file('GEO645+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ eqangle(u,v,w,x,y,z,w,x)
| para(u,v,y,z) ),
file('GEO645+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ para(u,v,w,x)
| eqangle(u,v,y,z,w,x,y,z) ),
file('GEO645+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ cyclic(u,v,w,x)
| eqangle(w,u,w,v,x,u,x,v) ),
file('GEO645+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ midp(u,v,w)
| ~ midp(x,v,y)
| para(x,u,y,w) ),
file('GEO645+1.p',unknown),
[] ).
cnf(37,axiom,
( ~ cong(u,v,u,w)
| eqangle(u,v,v,w,v,w,u,w) ),
file('GEO645+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ coll(u,v,w)
| ~ cong(u,v,u,w)
| midp(u,v,w) ),
file('GEO645+1.p',unknown),
[] ).
cnf(43,axiom,
( ~ para(u,v,w,x)
| ~ para(y,z,u,v)
| para(y,z,w,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ perp(u,v,w,x)
| ~ perp(y,z,u,v)
| para(y,z,w,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ perp(u,v,w,x)
| ~ para(y,z,u,v)
| perp(y,z,w,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(47,axiom,
( ~ cyclic(u,v,w,x)
| ~ cyclic(u,v,w,y)
| cyclic(v,w,y,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(49,axiom,
( ~ cong(u,v,w,v)
| ~ cong(u,x,w,x)
| perp(u,w,x,v) ),
file('GEO645+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(w,x,u,v,x1,x2,y,z) ),
file('GEO645+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(y,z,x1,x2,u,v,w,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(57,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(u,v,y,z,w,x,x1,x2) ),
file('GEO645+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ eqangle(u,v,u,w,x,v,x,w)
| coll(u,x,v)
| cyclic(v,w,u,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ coll(u,v,w)
| ~ perp(x,y,y,u)
| perp(skf36(w,v,x),x,v,w) ),
file('GEO645+1.p',unknown),
[] ).
cnf(78,axiom,
( ~ coll(u,v,w)
| ~ midp(x,v,y)
| ~ para(x,u,y,w)
| midp(u,v,w) ),
file('GEO645+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ coll(u,v,w)
| ~ eqangle(u,x,u,w,v,x,v,w)
| cyclic(x,w,u,v) ),
file('GEO645+1.p',unknown),
[] ).
cnf(86,axiom,
( ~ perp(u,v,w,x)
| ~ eqangle(y,z,x1,x2,u,v,w,x)
| perp(y,z,x1,x2) ),
file('GEO645+1.p',unknown),
[] ).
cnf(87,axiom,
( ~ para(u,v,w,x)
| ~ eqangle(y,z,x1,x2,u,v,w,x)
| para(y,z,x1,x2) ),
file('GEO645+1.p',unknown),
[] ).
cnf(88,axiom,
( ~ midp(u,v,w)
| ~ para(v,x,w,y)
| ~ para(v,y,w,x)
| midp(u,y,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(90,axiom,
( ~ para(u,v,w,x)
| ~ cyclic(u,v,w,x)
| eqangle(u,x,w,x,w,x,w,v) ),
file('GEO645+1.p',unknown),
[] ).
cnf(92,axiom,
( ~ perp(u,v,v,w)
| ~ circle(u,v,x,y)
| eqangle(v,w,v,x,y,v,y,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(95,axiom,
( ~ cyclic(u,v,w,x)
| ~ cong(u,x,v,x)
| ~ cong(u,w,v,w)
| perp(w,u,u,x) ),
file('GEO645+1.p',unknown),
[] ).
cnf(121,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('GEO645+1.p',unknown),
[] ).
cnf(123,plain,
( ~ coll(skc12,skc13,u)
| coll(skc10,u,skc12) ),
inference(res,[status(thm),theory(equality)],[2,26]),
[iquote('0:Res:2.0,26.0')] ).
cnf(125,plain,
coll(skc13,skc12,skc10),
inference(res,[status(thm),theory(equality)],[2,10]),
[iquote('0:Res:2.0,10.0')] ).
cnf(147,plain,
coll(skc11,skc9,skc13),
inference(res,[status(thm),theory(equality)],[1,9]),
[iquote('0:Res:1.0,9.0')] ).
cnf(169,plain,
( ~ perp(skc14,skc13,skc13,u)
| eqangle(skc13,u,skc13,skc11,skc17,skc13,skc17,skc11) ),
inference(res,[status(thm),theory(equality)],[7,92]),
[iquote('0:Res:7.0,92.0')] ).
cnf(188,plain,
perp(skc9,skc13,skc14,skc9),
inference(res,[status(thm),theory(equality)],[6,18]),
[iquote('0:Res:6.0,18.0')] ).
cnf(189,plain,
( ~ coll(skc13,u,v)
| perp(skf36(v,u,skc14),skc14,u,v) ),
inference(res,[status(thm),theory(equality)],[6,67]),
[iquote('0:Res:6.0,67.0')] ).
cnf(208,plain,
( ~ eqangle(u,v,w,x,skc14,skc9,skc9,skc13)
| perp(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[6,86]),
[iquote('0:Res:6.0,86.1')] ).
cnf(217,plain,
( ~ perp(skc10,skc13,u,v)
| para(skc14,skc10,u,v) ),
inference(res,[status(thm),theory(equality)],[5,44]),
[iquote('0:Res:5.0,44.0')] ).
cnf(219,plain,
perp(skc10,skc13,skc14,skc10),
inference(res,[status(thm),theory(equality)],[5,18]),
[iquote('0:Res:5.0,18.0')] ).
cnf(228,plain,
( ~ perp(u,v,skc14,skc10)
| para(u,v,skc10,skc13) ),
inference(res,[status(thm),theory(equality)],[5,44]),
[iquote('0:Res:5.0,44.1')] ).
cnf(269,plain,
coll(skc13,skc10,skc12),
inference(res,[status(thm),theory(equality)],[125,9]),
[iquote('0:Res:125.0,9.0')] ).
cnf(310,plain,
( ~ perp(skc10,skc13,u,v)
| para(skc14,skc10,v,u) ),
inference(res,[status(thm),theory(equality)],[217,15]),
[iquote('0:Res:217.1,15.0')] ).
cnf(316,plain,
( ~ perp(skc10,u,skc14,skc10)
| coll(skc10,u,skc13) ),
inference(res,[status(thm),theory(equality)],[228,13]),
[iquote('0:Res:228.1,13.0')] ).
cnf(318,plain,
( ~ perp(u,v,skc14,skc10)
| para(skc10,skc13,u,v) ),
inference(res,[status(thm),theory(equality)],[228,16]),
[iquote('0:Res:228.1,16.0')] ).
cnf(319,plain,
coll(skc10,skc13,skc13),
inference(res,[status(thm),theory(equality)],[219,316]),
[iquote('0:Res:219.0,316.0')] ).
cnf(326,plain,
coll(skc13,skc10,skc13),
inference(res,[status(thm),theory(equality)],[319,10]),
[iquote('0:Res:319.0,10.0')] ).
cnf(327,plain,
coll(skc13,skc13,skc10),
inference(res,[status(thm),theory(equality)],[326,9]),
[iquote('0:Res:326.0,9.0')] ).
cnf(405,plain,
( ~ coll(skc13,skc13,u)
| coll(u,skc10,skc13) ),
inference(res,[status(thm),theory(equality)],[327,26]),
[iquote('0:Res:327.0,26.0')] ).
cnf(406,plain,
( ~ coll(skc13,skc10,u)
| coll(u,skc12,skc13) ),
inference(res,[status(thm),theory(equality)],[269,26]),
[iquote('0:Res:269.0,26.0')] ).
cnf(407,plain,
( ~ coll(skc11,skc9,u)
| coll(u,skc13,skc11) ),
inference(res,[status(thm),theory(equality)],[147,26]),
[iquote('0:Res:147.0,26.0')] ).
cnf(507,plain,
coll(skc13,skc13,skc11),
inference(res,[status(thm),theory(equality)],[147,407]),
[iquote('0:Res:147.0,407.0')] ).
cnf(509,plain,
coll(skc11,skc10,skc13),
inference(res,[status(thm),theory(equality)],[507,405]),
[iquote('0:Res:507.0,405.0')] ).
cnf(514,plain,
coll(skc11,skc13,skc10),
inference(res,[status(thm),theory(equality)],[509,9]),
[iquote('0:Res:509.0,9.0')] ).
cnf(524,plain,
coll(skc13,skc11,skc10),
inference(res,[status(thm),theory(equality)],[514,10]),
[iquote('0:Res:514.0,10.0')] ).
cnf(544,plain,
coll(skc13,skc10,skc11),
inference(res,[status(thm),theory(equality)],[524,9]),
[iquote('0:Res:524.0,9.0')] ).
cnf(565,plain,
coll(skc11,skc12,skc13),
inference(res,[status(thm),theory(equality)],[544,406]),
[iquote('0:Res:544.0,406.0')] ).
cnf(584,plain,
coll(skc12,skc11,skc13),
inference(res,[status(thm),theory(equality)],[565,10]),
[iquote('0:Res:565.0,10.0')] ).
cnf(592,plain,
( ~ cong(u,u,u,v)
| para(u,u,u,v) ),
inference(res,[status(thm),theory(equality)],[37,33]),
[iquote('0:Res:37.1,33.0')] ).
cnf(594,plain,
( ~ cyclic(u,v,w,w)
| para(w,u,w,u) ),
inference(res,[status(thm),theory(equality)],[35,33]),
[iquote('0:Res:35.1,33.0')] ).
cnf(601,plain,
coll(skc12,skc13,skc11),
inference(res,[status(thm),theory(equality)],[584,9]),
[iquote('0:Res:584.0,9.0')] ).
cnf(654,plain,
coll(skc10,skc11,skc12),
inference(res,[status(thm),theory(equality)],[601,123]),
[iquote('0:Res:601.0,123.0')] ).
cnf(691,plain,
coll(skc10,skc12,skc11),
inference(res,[status(thm),theory(equality)],[654,9]),
[iquote('0:Res:654.0,9.0')] ).
cnf(721,plain,
coll(skc12,skc10,skc11),
inference(res,[status(thm),theory(equality)],[691,10]),
[iquote('0:Res:691.0,10.0')] ).
cnf(735,plain,
( ~ coll(skc12,skc10,u)
| coll(u,skc11,skc12) ),
inference(res,[status(thm),theory(equality)],[721,26]),
[iquote('0:Res:721.0,26.0')] ).
cnf(843,plain,
( ~ para(u,v,skc9,skc13)
| perp(u,v,skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[188,45]),
[iquote('0:Res:188.0,45.0')] ).
cnf(1172,plain,
( ~ para(u,v,u,v)
| coll(u,u,v)
| cyclic(v,w,u,u) ),
inference(res,[status(thm),theory(equality)],[34,62]),
[iquote('0:Res:34.1,62.0')] ).
cnf(1245,plain,
( ~ para(u,v,w,x)
| eqangle(u,v,w,x,y,z,y,z) ),
inference(res,[status(thm),theory(equality)],[34,57]),
[iquote('0:Res:34.1,57.0')] ).
cnf(1260,plain,
( ~ cong(u,v,u,w)
| eqangle(v,w,u,w,u,v,v,w) ),
inference(res,[status(thm),theory(equality)],[37,56]),
[iquote('0:Res:37.1,56.0')] ).
cnf(1277,plain,
( ~ para(u,v,w,x)
| eqangle(y,z,u,v,y,z,w,x) ),
inference(res,[status(thm),theory(equality)],[34,55]),
[iquote('0:Res:34.1,55.0')] ).
cnf(1517,plain,
( ~ para(u,v,u,v)
| ~ coll(u,u,w)
| cyclic(v,w,u,u) ),
inference(res,[status(thm),theory(equality)],[34,79]),
[iquote('0:Res:34.1,79.1')] ).
cnf(1774,plain,
( ~ cyclic(u,v,w,x)
| ~ para(x,u,x,v)
| para(w,u,w,v) ),
inference(res,[status(thm),theory(equality)],[35,87]),
[iquote('0:Res:35.1,87.1')] ).
cnf(2382,plain,
( ~ para(u,v,u,w)
| ~ cyclic(v,x,u,w)
| ~ cyclic(v,x,u,x)
| ~ cyclic(v,x,u,u)
| cong(v,x,w,x) ),
inference(res,[status(thm),theory(equality)],[34,121]),
[iquote('0:Res:34.1,121.3')] ).
cnf(2384,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)],[90,121]),
[iquote('0:Res:90.2,121.3')] ).
cnf(2385,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)],[35,121]),
[iquote('0:Res:35.1,121.3')] ).
cnf(2387,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)],[2385]),
[iquote('0:Obv:2385.0')] ).
cnf(2388,plain,
( ~ cyclic(u,v,w,u)
| ~ cyclic(u,v,w,v)
| cong(u,v,u,v) ),
inference(con,[status(thm)],[2387]),
[iquote('0:Con:2387.2')] ).
cnf(2868,plain,
( ~ coll(skc13,u,v)
| ~ para(w,x,skf36(v,u,skc14),skc14)
| perp(w,x,u,v) ),
inference(res,[status(thm),theory(equality)],[189,45]),
[iquote('0:Res:189.1,45.0')] ).
cnf(3668,plain,
( ~ perp(skc14,skc13,skc13,skc13)
| ~ coll(skc13,skc17,skc11)
| cyclic(skc13,skc11,skc13,skc17) ),
inference(res,[status(thm),theory(equality)],[169,79]),
[iquote('0:Res:169.1,79.1')] ).
cnf(3671,plain,
( ~ perp(skc14,skc13,skc13,u)
| ~ para(skc17,skc13,skc17,skc11)
| para(skc13,u,skc13,skc11) ),
inference(res,[status(thm),theory(equality)],[169,87]),
[iquote('0:Res:169.1,87.1')] ).
cnf(4593,plain,
( ~ para(u,v,u,v)
| coll(u,w,v)
| cyclic(v,v,u,w) ),
inference(res,[status(thm),theory(equality)],[1245,62]),
[iquote('0:Res:1245.1,62.0')] ).
cnf(4604,plain,
( ~ para(u,v,u,v)
| ~ coll(u,w,v)
| cyclic(v,v,u,w) ),
inference(res,[status(thm),theory(equality)],[1245,79]),
[iquote('0:Res:1245.1,79.1')] ).
cnf(4618,plain,
( ~ para(u,v,u,v)
| cyclic(v,v,u,w) ),
inference(mrr,[status(thm)],[4604,4593]),
[iquote('0:MRR:4604.1,4593.1')] ).
cnf(4726,plain,
( ~ cong(u,u,u,v)
| para(u,v,u,u) ),
inference(res,[status(thm),theory(equality)],[1260,33]),
[iquote('0:Res:1260.1,33.0')] ).
cnf(4916,plain,
( ~ para(u,v,u,v)
| para(w,x,w,x) ),
inference(res,[status(thm),theory(equality)],[1277,33]),
[iquote('0:Res:1277.1,33.0')] ).
cnf(4923,plain,
( ~ para(u,v,skc9,skc13)
| perp(skc14,skc9,u,v) ),
inference(res,[status(thm),theory(equality)],[1277,208]),
[iquote('0:Res:1277.1,208.0')] ).
cnf(5194,plain,
( ~ perp(skc10,skc13,skc14,skc10)
| ~ coll(skc10,skc10,u)
| cyclic(skc13,u,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[228,1517]),
[iquote('0:Res:228.1,1517.0')] ).
cnf(5198,plain,
( ~ coll(skc10,skc10,u)
| cyclic(skc13,u,skc10,skc10) ),
inference(mrr,[status(thm)],[5194,219]),
[iquote('0:MRR:5194.0,219.0')] ).
cnf(9053,plain,
( ~ perp(skc10,u,skc14,skc10)
| ~ cyclic(skc10,u,skc10,skc13)
| ~ cyclic(skc13,skc13,skc10,skc13)
| ~ cyclic(skc13,skc13,skc10,u)
| ~ cyclic(skc13,skc13,skc10,skc10)
| cong(skc13,skc13,skc13,u) ),
inference(res,[status(thm),theory(equality)],[228,2384]),
[iquote('0:Res:228.1,2384.0')] ).
cnf(9574,plain,
( ~ coll(skc10,skc10,u)
| cyclic(u,skc13,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[5198,21]),
[iquote('0:Res:5198.1,21.0')] ).
cnf(10343,plain,
( ~ perp(skc10,skc13,u,v)
| ~ para(w,x,skc14,skc10)
| para(w,x,v,u) ),
inference(res,[status(thm),theory(equality)],[310,43]),
[iquote('0:Res:310.1,43.0')] ).
cnf(10494,plain,
( ~ perp(skc10,u,skc14,skc10)
| ~ cyclic(skc13,v,skc10,u)
| ~ cyclic(skc13,v,skc10,v)
| ~ cyclic(skc13,v,skc10,skc10)
| cong(skc13,v,u,v) ),
inference(res,[status(thm),theory(equality)],[318,2382]),
[iquote('0:Res:318.1,2382.0')] ).
cnf(10498,plain,
( ~ perp(skc10,u,skc14,skc10)
| coll(skc10,skc13,u) ),
inference(res,[status(thm),theory(equality)],[318,13]),
[iquote('0:Res:318.1,13.0')] ).
cnf(10953,plain,
( ~ perp(skc10,skc13,skc13,skc9)
| perp(skc14,skc9,skc14,skc10) ),
inference(res,[status(thm),theory(equality)],[310,4923]),
[iquote('0:Res:310.1,4923.0')] ).
cnf(11046,plain,
( ~ perp(skc10,skc13,skc14,skc10)
| cyclic(skc10,skc10,skc14,u) ),
inference(res,[status(thm),theory(equality)],[217,4618]),
[iquote('0:Res:217.1,4618.0')] ).
cnf(11050,plain,
( ~ perp(skc10,skc13,skc14,skc10)
| cyclic(skc13,skc13,skc10,u) ),
inference(res,[status(thm),theory(equality)],[228,4618]),
[iquote('0:Res:228.1,4618.0')] ).
cnf(11062,plain,
cyclic(skc10,skc10,skc14,u),
inference(mrr,[status(thm)],[11046,219]),
[iquote('0:MRR:11046.0,219.0')] ).
cnf(11068,plain,
cyclic(skc13,skc13,skc10,u),
inference(mrr,[status(thm)],[11050,219]),
[iquote('0:MRR:11050.0,219.0')] ).
cnf(11069,plain,
( ~ perp(skc10,u,skc14,skc10)
| ~ cyclic(skc10,u,skc10,skc13)
| cong(skc13,skc13,skc13,u) ),
inference(mrr,[status(thm)],[9053,11068]),
[iquote('0:MRR:9053.4,9053.2,9053.3,11068.0')] ).
cnf(11079,plain,
( ~ cong(skc10,u,skc10,u)
| ~ cong(skc10,skc14,skc10,skc14)
| perp(skc14,skc10,skc10,u) ),
inference(res,[status(thm),theory(equality)],[11062,95]),
[iquote('0:Res:11062.0,95.0')] ).
cnf(11080,plain,
( ~ cyclic(skc10,skc10,skc14,u)
| cyclic(skc10,skc14,u,v) ),
inference(res,[status(thm),theory(equality)],[11062,47]),
[iquote('0:Res:11062.0,47.0')] ).
cnf(11084,plain,
para(skc14,skc10,skc14,skc10),
inference(res,[status(thm),theory(equality)],[11062,594]),
[iquote('0:Res:11062.0,594.0')] ).
cnf(11088,plain,
cyclic(skc10,skc14,u,v),
inference(mrr,[status(thm)],[11080,11062]),
[iquote('0:MRR:11080.0,11062.0')] ).
cnf(11433,plain,
para(u,v,u,v),
inference(res,[status(thm),theory(equality)],[11084,4916]),
[iquote('0:Res:11084.0,4916.0')] ).
cnf(11453,plain,
( coll(u,u,v)
| cyclic(v,w,u,u) ),
inference(mrr,[status(thm)],[1172,11433]),
[iquote('0:MRR:1172.0,11433.0')] ).
cnf(11525,plain,
cyclic(u,skc13,skc10,skc10),
inference(mrr,[status(thm)],[9574,11453]),
[iquote('0:MRR:9574.0,11453.0')] ).
cnf(11564,plain,
cyclic(u,skc10,skc13,skc10),
inference(res,[status(thm),theory(equality)],[11525,20]),
[iquote('0:Res:11525.0,20.0')] ).
cnf(11565,plain,
cyclic(skc13,u,skc10,skc10),
inference(res,[status(thm),theory(equality)],[11525,21]),
[iquote('0:Res:11525.0,21.0')] ).
cnf(11568,plain,
( ~ cyclic(skc10,skc13,skc10,skc13)
| cong(skc10,skc13,skc10,skc13) ),
inference(res,[status(thm),theory(equality)],[11525,2388]),
[iquote('0:Res:11525.0,2388.0')] ).
cnf(11571,plain,
( ~ perp(skc10,u,skc14,skc10)
| ~ cyclic(skc13,v,skc10,u)
| ~ cyclic(skc13,v,skc10,v)
| cong(skc13,v,u,v) ),
inference(mrr,[status(thm)],[10494,11565]),
[iquote('0:MRR:10494.3,11565.0')] ).
cnf(11758,plain,
cyclic(u,skc10,skc10,skc13),
inference(res,[status(thm),theory(equality)],[11564,19]),
[iquote('0:Res:11564.0,19.0')] ).
cnf(11760,plain,
cyclic(skc10,u,skc13,skc10),
inference(res,[status(thm),theory(equality)],[11564,21]),
[iquote('0:Res:11564.0,21.0')] ).
cnf(11877,plain,
cyclic(skc10,u,skc10,skc13),
inference(res,[status(thm),theory(equality)],[11758,21]),
[iquote('0:Res:11758.0,21.0')] ).
cnf(11882,plain,
( ~ perp(skc10,u,skc14,skc10)
| cong(skc13,skc13,skc13,u) ),
inference(mrr,[status(thm)],[11069,11877]),
[iquote('0:MRR:11069.1,11877.0')] ).
cnf(11883,plain,
cong(skc10,skc13,skc10,skc13),
inference(mrr,[status(thm)],[11568,11877]),
[iquote('0:MRR:11568.0,11877.0')] ).
cnf(11902,plain,
( ~ cong(skc10,u,skc10,u)
| perp(skc10,skc10,u,skc13) ),
inference(res,[status(thm),theory(equality)],[11883,49]),
[iquote('0:Res:11883.0,49.0')] ).
cnf(12045,plain,
cyclic(skc10,skc13,u,skc10),
inference(res,[status(thm),theory(equality)],[11760,20]),
[iquote('0:Res:11760.0,20.0')] ).
cnf(12047,plain,
( ~ cyclic(skc10,u,skc13,u)
| cong(skc10,u,skc10,u) ),
inference(res,[status(thm),theory(equality)],[11760,2388]),
[iquote('0:Res:11760.0,2388.0')] ).
cnf(12100,plain,
cyclic(skc10,skc13,skc10,u),
inference(res,[status(thm),theory(equality)],[12045,19]),
[iquote('0:Res:12045.0,19.0')] ).
cnf(12126,plain,
( ~ cyclic(skc10,skc13,skc10,u)
| cyclic(skc13,skc10,u,v) ),
inference(res,[status(thm),theory(equality)],[12100,47]),
[iquote('0:Res:12100.0,47.0')] ).
cnf(12133,plain,
cyclic(skc13,skc10,u,v),
inference(mrr,[status(thm)],[12126,12100]),
[iquote('0:MRR:12126.0,12100.0')] ).
cnf(12151,plain,
( ~ cyclic(skc10,skc14,u,skc14)
| cong(skc10,skc14,skc10,skc14) ),
inference(res,[status(thm),theory(equality)],[11088,2388]),
[iquote('0:Res:11088.0,2388.0')] ).
cnf(12206,plain,
cong(skc10,skc14,skc10,skc14),
inference(mrr,[status(thm)],[12151,11088]),
[iquote('0:MRR:12151.0,11088.0')] ).
cnf(12207,plain,
( ~ cong(skc10,u,skc10,u)
| perp(skc14,skc10,skc10,u) ),
inference(mrr,[status(thm)],[11079,12206]),
[iquote('0:MRR:11079.1,12206.0')] ).
cnf(12226,plain,
( ~ cong(skc10,u,skc10,u)
| perp(skc10,skc10,u,skc14) ),
inference(res,[status(thm),theory(equality)],[12206,49]),
[iquote('0:Res:12206.0,49.0')] ).
cnf(12838,plain,
( ~ cong(skc13,u,skc10,u)
| ~ cong(skc13,v,skc10,v)
| perp(v,skc13,skc13,u) ),
inference(res,[status(thm),theory(equality)],[12133,95]),
[iquote('0:Res:12133.0,95.0')] ).
cnf(12839,plain,
( ~ cyclic(skc13,skc10,u,v)
| cyclic(skc10,u,v,w) ),
inference(res,[status(thm),theory(equality)],[12133,47]),
[iquote('0:Res:12133.0,47.0')] ).
cnf(12841,plain,
cyclic(skc13,u,skc10,v),
inference(res,[status(thm),theory(equality)],[12133,20]),
[iquote('0:Res:12133.0,20.0')] ).
cnf(12848,plain,
( ~ perp(skc10,u,skc14,skc10)
| cong(skc13,v,u,v) ),
inference(mrr,[status(thm)],[11571,12841]),
[iquote('0:MRR:11571.2,11571.1,12841.0')] ).
cnf(12858,plain,
cyclic(skc10,u,v,w),
inference(mrr,[status(thm)],[12839,12133]),
[iquote('0:MRR:12839.0,12133.0')] ).
cnf(12861,plain,
cong(skc10,u,skc10,u),
inference(mrr,[status(thm)],[12047,12858]),
[iquote('0:MRR:12047.0,12858.0')] ).
cnf(12865,plain,
perp(skc10,skc10,u,skc13),
inference(mrr,[status(thm)],[11902,12861]),
[iquote('0:MRR:11902.0,12861.0')] ).
cnf(12866,plain,
perp(skc14,skc10,skc10,u),
inference(mrr,[status(thm)],[12207,12861]),
[iquote('0:MRR:12207.0,12861.0')] ).
cnf(12867,plain,
perp(skc10,skc10,u,skc14),
inference(mrr,[status(thm)],[12226,12861]),
[iquote('0:MRR:12226.0,12861.0')] ).
cnf(12950,plain,
perp(u,skc13,skc10,skc10),
inference(res,[status(thm),theory(equality)],[12865,18]),
[iquote('0:Res:12865.0,18.0')] ).
cnf(12987,plain,
perp(skc10,u,skc14,skc10),
inference(res,[status(thm),theory(equality)],[12866,18]),
[iquote('0:Res:12866.0,18.0')] ).
cnf(13016,plain,
coll(skc10,skc13,u),
inference(mrr,[status(thm)],[10498,12987]),
[iquote('0:MRR:10498.0,12987.0')] ).
cnf(13019,plain,
cong(skc13,skc13,skc13,u),
inference(mrr,[status(thm)],[11882,12987]),
[iquote('0:MRR:11882.0,12987.0')] ).
cnf(13023,plain,
cong(skc13,u,v,u),
inference(mrr,[status(thm)],[12848,12987]),
[iquote('0:MRR:12848.0,12987.0')] ).
cnf(13106,plain,
perp(u,skc13,skc13,v),
inference(mrr,[status(thm)],[12838,13023]),
[iquote('0:MRR:12838.1,12838.0,13023.0')] ).
cnf(13117,plain,
( ~ para(skc17,skc13,skc17,skc11)
| para(skc13,u,skc13,skc11) ),
inference(mrr,[status(thm)],[3671,13106]),
[iquote('0:MRR:3671.0,13106.0')] ).
cnf(13124,plain,
( ~ coll(skc13,skc17,skc11)
| cyclic(skc13,skc11,skc13,skc17) ),
inference(mrr,[status(thm)],[3668,13106]),
[iquote('0:MRR:3668.0,13106.0')] ).
cnf(13127,plain,
perp(skc14,skc9,skc14,skc10),
inference(mrr,[status(thm)],[10953,13106]),
[iquote('0:MRR:10953.0,13106.0')] ).
cnf(13166,plain,
( ~ coll(skc10,skc13,u)
| coll(u,v,skc10) ),
inference(res,[status(thm),theory(equality)],[13016,26]),
[iquote('0:Res:13016.0,26.0')] ).
cnf(13210,plain,
coll(u,v,skc10),
inference(mrr,[status(thm)],[13166,13016]),
[iquote('0:MRR:13166.0,13016.0')] ).
cnf(13285,plain,
coll(u,skc10,v),
inference(res,[status(thm),theory(equality)],[13210,9]),
[iquote('0:Res:13210.0,9.0')] ).
cnf(13309,plain,
coll(u,skc11,skc12),
inference(mrr,[status(thm)],[735,13285]),
[iquote('0:MRR:735.0,13285.0')] ).
cnf(13671,plain,
coll(skc11,u,skc12),
inference(res,[status(thm),theory(equality)],[13309,10]),
[iquote('0:Res:13309.0,10.0')] ).
cnf(13782,plain,
coll(skc11,skc12,u),
inference(res,[status(thm),theory(equality)],[13671,9]),
[iquote('0:Res:13671.0,9.0')] ).
cnf(13885,plain,
( ~ coll(skc11,skc12,u)
| coll(u,v,skc11) ),
inference(res,[status(thm),theory(equality)],[13782,26]),
[iquote('0:Res:13782.0,26.0')] ).
cnf(13888,plain,
coll(u,v,skc11),
inference(mrr,[status(thm)],[13885,13782]),
[iquote('0:MRR:13885.0,13782.0')] ).
cnf(13889,plain,
cyclic(skc13,skc11,skc13,skc17),
inference(mrr,[status(thm)],[13124,13888]),
[iquote('0:MRR:13124.0,13888.0')] ).
cnf(14008,plain,
( ~ coll(u,skc10,v)
| coll(v,w,u) ),
inference(res,[status(thm),theory(equality)],[13285,26]),
[iquote('0:Res:13285.0,26.0')] ).
cnf(14023,plain,
coll(u,v,w),
inference(mrr,[status(thm)],[14008,13285]),
[iquote('0:MRR:14008.0,13285.0')] ).
cnf(14024,plain,
( ~ cong(u,v,u,w)
| midp(u,v,w) ),
inference(mrr,[status(thm)],[39,14023]),
[iquote('0:MRR:39.0,14023.0')] ).
cnf(14027,plain,
( ~ midp(u,v,w)
| ~ para(u,x,w,y)
| midp(x,v,y) ),
inference(mrr,[status(thm)],[78,14023]),
[iquote('0:MRR:78.0,14023.0')] ).
cnf(14114,plain,
( ~ para(u,v,skf36(w,x,skc14),skc14)
| perp(u,v,x,w) ),
inference(mrr,[status(thm)],[2868,14023]),
[iquote('0:MRR:2868.0,14023.0')] ).
cnf(14251,plain,
( ~ perp(u,v,skc14,skc9)
| para(u,v,skc14,skc10) ),
inference(res,[status(thm),theory(equality)],[13127,44]),
[iquote('0:Res:13127.0,44.0')] ).
cnf(14473,plain,
cyclic(skc13,skc11,skc17,skc13),
inference(res,[status(thm),theory(equality)],[13889,19]),
[iquote('0:Res:13889.0,19.0')] ).
cnf(14650,plain,
( ~ para(skc13,skc13,skc13,skc11)
| para(skc17,skc13,skc17,skc11) ),
inference(res,[status(thm),theory(equality)],[14473,1774]),
[iquote('0:Res:14473.0,1774.0')] ).
cnf(14655,plain,
cyclic(skc11,skc13,skc17,skc13),
inference(res,[status(thm),theory(equality)],[14473,21]),
[iquote('0:Res:14473.0,21.0')] ).
cnf(14788,plain,
( ~ para(skc13,skc11,skc13,skc13)
| para(skc17,skc11,skc17,skc13) ),
inference(res,[status(thm),theory(equality)],[14655,1774]),
[iquote('0:Res:14655.0,1774.0')] ).
cnf(14979,plain,
( ~ perp(u,v,skc10,skc10)
| para(u,v,w,skc14) ),
inference(res,[status(thm),theory(equality)],[12867,44]),
[iquote('0:Res:12867.0,44.0')] ).
cnf(15093,plain,
( ~ para(u,v,w,skc13)
| perp(u,v,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[12950,45]),
[iquote('0:Res:12950.0,45.0')] ).
cnf(15136,plain,
midp(skc13,skc13,u),
inference(res,[status(thm),theory(equality)],[13019,14024]),
[iquote('0:Res:13019.0,14024.0')] ).
cnf(15152,plain,
para(skc13,u,skc13,skc13),
inference(res,[status(thm),theory(equality)],[13019,4726]),
[iquote('0:Res:13019.0,4726.0')] ).
cnf(15153,plain,
para(skc13,skc13,skc13,u),
inference(res,[status(thm),theory(equality)],[13019,592]),
[iquote('0:Res:13019.0,592.0')] ).
cnf(16768,plain,
para(skc17,skc11,skc17,skc13),
inference(mrr,[status(thm)],[14788,15152]),
[iquote('0:MRR:14788.0,15152.0')] ).
cnf(16771,plain,
para(skc17,skc13,skc17,skc11),
inference(mrr,[status(thm)],[14650,15153]),
[iquote('0:MRR:14650.0,15153.0')] ).
cnf(16783,plain,
para(skc13,u,skc13,skc11),
inference(mrr,[status(thm)],[13117,16771]),
[iquote('0:MRR:13117.0,16771.0')] ).
cnf(17903,plain,
midp(skc13,u,skc13),
inference(res,[status(thm),theory(equality)],[15136,11]),
[iquote('0:Res:15136.0,11.0')] ).
cnf(18664,plain,
( ~ midp(u,skc17,skc17)
| ~ para(skc17,skc11,skc17,skc13)
| midp(u,skc11,skc13) ),
inference(res,[status(thm),theory(equality)],[16771,88]),
[iquote('0:Res:16771.0,88.1')] ).
cnf(18667,plain,
( ~ midp(u,skc17,skc17)
| midp(u,skc11,skc13) ),
inference(mrr,[status(thm)],[18664,16768]),
[iquote('0:MRR:18664.1,16768.0')] ).
cnf(18675,plain,
para(skc17,skc11,skc13,skc17),
inference(res,[status(thm),theory(equality)],[16768,15]),
[iquote('0:Res:16768.0,15.0')] ).
cnf(18885,plain,
para(skc13,skc17,skc17,skc11),
inference(res,[status(thm),theory(equality)],[18675,16]),
[iquote('0:Res:18675.0,16.0')] ).
cnf(19073,plain,
para(skc13,skc17,skc11,skc17),
inference(res,[status(thm),theory(equality)],[18885,15]),
[iquote('0:Res:18885.0,15.0')] ).
cnf(19238,plain,
( ~ midp(u,skc13,skc11)
| ~ para(skc13,skc17,skc11,skc17)
| midp(u,skc17,skc17) ),
inference(res,[status(thm),theory(equality)],[19073,88]),
[iquote('0:Res:19073.0,88.1')] ).
cnf(19241,plain,
( ~ midp(u,skc13,skc11)
| midp(u,skc17,skc17) ),
inference(mrr,[status(thm)],[19238,19073]),
[iquote('0:MRR:19238.1,19073.0')] ).
cnf(20682,plain,
( ~ midp(skc13,u,skc13)
| midp(v,u,skc11) ),
inference(res,[status(thm),theory(equality)],[16783,14027]),
[iquote('0:Res:16783.0,14027.1')] ).
cnf(20685,plain,
midp(u,v,skc11),
inference(mrr,[status(thm)],[20682,17903]),
[iquote('0:MRR:20682.0,17903.0')] ).
cnf(20694,plain,
midp(u,skc17,skc17),
inference(mrr,[status(thm)],[19241,20685]),
[iquote('0:MRR:19241.0,20685.0')] ).
cnf(20735,plain,
midp(u,skc11,skc13),
inference(mrr,[status(thm)],[18667,20694]),
[iquote('0:MRR:18667.0,20694.0')] ).
cnf(20874,plain,
( ~ midp(u,skc11,v)
| para(u,w,v,skc13) ),
inference(res,[status(thm),theory(equality)],[20735,36]),
[iquote('0:Res:20735.0,36.0')] ).
cnf(20914,plain,
midp(u,skc11,v),
inference(res,[status(thm),theory(equality)],[20685,11]),
[iquote('0:Res:20685.0,11.0')] ).
cnf(20918,plain,
para(u,v,w,skc13),
inference(mrr,[status(thm)],[20874,20914]),
[iquote('0:MRR:20874.0,20914.0')] ).
cnf(20946,plain,
perp(u,v,skc14,skc9),
inference(mrr,[status(thm)],[843,20918]),
[iquote('0:MRR:843.0,20918.0')] ).
cnf(20975,plain,
perp(u,v,skc10,skc10),
inference(mrr,[status(thm)],[15093,20918]),
[iquote('0:MRR:15093.0,20918.0')] ).
cnf(21080,plain,
para(u,v,skc14,skc10),
inference(mrr,[status(thm)],[14251,20946]),
[iquote('0:MRR:14251.0,20946.0')] ).
cnf(21246,plain,
para(u,v,w,skc14),
inference(mrr,[status(thm)],[14979,20975]),
[iquote('0:MRR:14979.0,20975.0')] ).
cnf(21354,plain,
( ~ perp(skc10,skc13,u,v)
| para(w,x,v,u) ),
inference(mrr,[status(thm)],[10343,21080]),
[iquote('0:MRR:10343.1,21080.0')] ).
cnf(21451,plain,
perp(u,v,w,x),
inference(mrr,[status(thm)],[14114,21246]),
[iquote('0:MRR:14114.0,21246.0')] ).
cnf(21527,plain,
para(u,v,w,x),
inference(mrr,[status(thm)],[21354,21451]),
[iquote('0:MRR:21354.0,21451.0')] ).
cnf(21528,plain,
$false,
inference(unc,[status(thm)],[21527,8]),
[iquote('0:UnC:21527.0,8.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : GEO645+1 : TPTP v8.1.0. Released v7.5.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n022.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 23:36:47 EDT 2022
% 0.12/0.33 % CPUTime :
% 14.40/14.61
% 14.40/14.61 SPASS V 3.9
% 14.40/14.61 SPASS beiseite: Proof found.
% 14.40/14.61 % SZS status Theorem
% 14.40/14.61 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.40/14.61 SPASS derived 19941 clauses, backtracked 2474 clauses, performed 4 splits and kept 14049 clauses.
% 14.40/14.61 SPASS allocated 100091 KBytes.
% 14.40/14.61 SPASS spent 0:0:14.25 on the problem.
% 14.40/14.61 0:00:00.04 for the input.
% 14.40/14.61 0:00:00.24 for the FLOTTER CNF translation.
% 14.40/14.61 0:00:00.44 for inferences.
% 14.40/14.61 0:00:00.04 for the backtracking.
% 14.40/14.61 0:0:13.08 for the reduction.
% 14.40/14.61
% 14.40/14.61
% 14.40/14.61 Here is a proof with depth 20, length 204 :
% 14.40/14.61 % SZS output start Refutation
% See solution above
% 14.49/14.67 Formulae used in the proof : exemplo6GDDFULLmoreE0091 ruleD1 ruleD2 ruleD11 ruleD66 ruleD4 ruleD5 ruleD8 ruleD14 ruleD15 ruleD16 ruleD3 ruleD39 ruleD40 ruleD41 ruleD44 ruleD46 ruleD67 ruleD6 ruleD9 ruleD10 ruleD17 ruleD56 ruleD19 ruleD20 ruleD21 ruleD42a ruleX15 ruleD45 ruleD42b ruleD74 ruleD73 ruleD64 ruleD54 ruleD48 ruleD57 ruleD43
% 14.49/14.67
%------------------------------------------------------------------------------