%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GEO622+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n021.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:34 EDT 2022
% Result : Theorem 11.09s 11.36s
% Output : Refutation 11.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 27
% Syntax : Number of clauses : 92 ( 38 unt; 5 nHn; 92 RR)
% Number of literals : 175 ( 0 equ; 81 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 14 ( 14 usr; 13 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
coll(skc9,skc7,skc8),
file('GEO622+1.p',unknown),
[] ).
cnf(6,axiom,
~ perp(skc9,skc10,skc7,skc8),
file('GEO622+1.p',unknown),
[] ).
cnf(7,axiom,
eqangle(skc9,skc11,skc11,skc8,skc9,skc11,skc11,skc7),
file('GEO622+1.p',unknown),
[] ).
cnf(8,axiom,
( ~ coll(u,v,w)
| coll(u,w,v) ),
file('GEO622+1.p',unknown),
[] ).
cnf(9,axiom,
( ~ coll(u,v,w)
| coll(v,u,w) ),
file('GEO622+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ para(u,v,w,x)
| para(w,x,u,v) ),
file('GEO622+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(u,w,v,x) ),
file('GEO622+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ cyclic(u,v,w,x)
| cyclic(v,u,w,x) ),
file('GEO622+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ coll(u,v,w)
| ~ coll(u,v,x)
| coll(x,w,u) ),
file('GEO622+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ eqangle(u,v,w,x,y,z,w,x)
| para(u,v,y,z) ),
file('GEO622+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ para(u,v,w,x)
| eqangle(u,v,y,z,w,x,y,z) ),
file('GEO622+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ cyclic(u,v,w,x)
| eqangle(w,u,w,v,x,u,x,v) ),
file('GEO622+1.p',unknown),
[] ).
cnf(38,axiom,
( ~ coll(u,v,w)
| ~ cong(u,v,u,w)
| midp(u,v,w) ),
file('GEO622+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ midp(u,v,w)
| ~ perp(v,x,x,w)
| cong(v,u,x,u) ),
file('GEO622+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ cyclic(u,v,w,x)
| ~ cyclic(u,v,w,y)
| cyclic(v,w,y,x) ),
file('GEO622+1.p',unknown),
[] ).
cnf(48,axiom,
( ~ cong(u,v,w,v)
| ~ cong(u,x,w,x)
| perp(u,w,x,v) ),
file('GEO622+1.p',unknown),
[] ).
cnf(53,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(v,u,w,x,y,z,x1,x2) ),
file('GEO622+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(w,x,u,v,x1,x2,y,z) ),
file('GEO622+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(y,z,x1,x2,u,v,w,x) ),
file('GEO622+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ eqangle(u,v,w,x,y,z,x1,x2)
| eqangle(u,v,y,z,w,x,x1,x2) ),
file('GEO622+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ eqangle(u,v,u,w,x,v,x,w)
| coll(u,x,v)
| cyclic(v,w,u,x) ),
file('GEO622+1.p',unknown),
[] ).
cnf(68,axiom,
( ~ perp(u,v,v,w)
| ~ cyclic(u,w,v,x)
| circle(skf35(v,w,u),u,w,v) ),
file('GEO622+1.p',unknown),
[] ).
cnf(78,axiom,
( ~ coll(u,v,w)
| ~ eqangle(u,x,u,w,v,x,v,w)
| cyclic(x,w,u,v) ),
file('GEO622+1.p',unknown),
[] ).
cnf(86,axiom,
( ~ para(u,v,w,x)
| ~ eqangle(y,z,x1,x2,u,v,w,x)
| para(y,z,x1,x2) ),
file('GEO622+1.p',unknown),
[] ).
cnf(91,axiom,
( ~ perp(u,v,v,w)
| ~ circle(u,v,x,y)
| eqangle(v,w,v,x,y,v,y,x) ),
file('GEO622+1.p',unknown),
[] ).
cnf(94,axiom,
( ~ cyclic(u,v,w,x)
| ~ cong(u,x,v,x)
| ~ cong(u,w,v,w)
| perp(w,u,u,x) ),
file('GEO622+1.p',unknown),
[] ).
cnf(120,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('GEO622+1.p',unknown),
[] ).
cnf(121,plain,
( ~ cong(skc9,skc7,skc9,skc8)
| midp(skc9,skc7,skc8) ),
inference(res,[status(thm),theory(equality)],[3,38]),
[iquote('0:Res:3.0,38.1')] ).
cnf(123,plain,
coll(skc9,skc8,skc7),
inference(res,[status(thm),theory(equality)],[3,8]),
[iquote('0:Res:3.0,8.0')] ).
cnf(126,plain,
( ~ coll(skc9,skc7,u)
| coll(u,skc8,skc9) ),
inference(res,[status(thm),theory(equality)],[3,25]),
[iquote('0:Res:3.0,25.1')] ).
cnf(201,plain,
( ~ cong(skc9,skc8,skc10,skc8)
| ~ cong(skc9,skc7,skc10,skc7) ),
inference(res,[status(thm),theory(equality)],[48,6]),
[iquote('0:Res:48.2,6.0')] ).
cnf(206,plain,
eqangle(skc11,skc9,skc11,skc8,skc9,skc11,skc11,skc7),
inference(res,[status(thm),theory(equality)],[7,53]),
[iquote('0:Res:7.0,53.0')] ).
cnf(207,plain,
eqangle(skc11,skc8,skc9,skc11,skc11,skc7,skc9,skc11),
inference(res,[status(thm),theory(equality)],[7,54]),
[iquote('0:Res:7.0,54.0')] ).
cnf(225,plain,
coll(skc8,skc8,skc9),
inference(res,[status(thm),theory(equality)],[3,126]),
[iquote('0:Res:3.0,126.0')] ).
cnf(396,plain,
( ~ coll(skc9,skc8,u)
| coll(u,skc7,skc9) ),
inference(res,[status(thm),theory(equality)],[123,25]),
[iquote('0:Res:123.0,25.0')] ).
cnf(398,plain,
( ~ coll(skc8,skc8,u)
| coll(u,skc9,skc8) ),
inference(res,[status(thm),theory(equality)],[225,25]),
[iquote('0:Res:225.0,25.0')] ).
cnf(534,plain,
coll(skc9,skc9,skc8),
inference(res,[status(thm),theory(equality)],[225,398]),
[iquote('0:Res:225.0,398.0')] ).
cnf(538,plain,
coll(skc9,skc8,skc9),
inference(res,[status(thm),theory(equality)],[534,8]),
[iquote('0:Res:534.0,8.0')] ).
cnf(541,plain,
coll(skc9,skc7,skc9),
inference(res,[status(thm),theory(equality)],[538,396]),
[iquote('0:Res:538.0,396.0')] ).
cnf(549,plain,
coll(skc7,skc9,skc9),
inference(res,[status(thm),theory(equality)],[541,9]),
[iquote('0:Res:541.0,9.0')] ).
cnf(588,plain,
para(skc11,skc8,skc11,skc7),
inference(res,[status(thm),theory(equality)],[207,32]),
[iquote('0:Res:207.0,32.0')] ).
cnf(730,plain,
para(skc11,skc7,skc11,skc8),
inference(res,[status(thm),theory(equality)],[588,15]),
[iquote('0:Res:588.0,15.0')] ).
cnf(1094,plain,
( ~ para(u,v,u,v)
| coll(u,u,v)
| cyclic(v,w,u,u) ),
inference(res,[status(thm),theory(equality)],[33,61]),
[iquote('0:Res:33.1,61.0')] ).
cnf(1179,plain,
eqangle(skc11,skc9,skc9,skc11,skc11,skc8,skc11,skc7),
inference(res,[status(thm),theory(equality)],[206,56]),
[iquote('0:Res:206.0,56.0')] ).
cnf(1181,plain,
( ~ para(u,v,w,x)
| eqangle(u,v,w,x,y,z,y,z) ),
inference(res,[status(thm),theory(equality)],[33,56]),
[iquote('0:Res:33.1,56.0')] ).
cnf(1202,plain,
eqangle(skc9,skc11,skc11,skc7,skc11,skc9,skc11,skc8),
inference(res,[status(thm),theory(equality)],[206,55]),
[iquote('0:Res:206.0,55.0')] ).
cnf(1228,plain,
( ~ para(u,v,w,x)
| eqangle(y,z,u,v,y,z,w,x) ),
inference(res,[status(thm),theory(equality)],[33,54]),
[iquote('0:Res:33.1,54.0')] ).
cnf(1476,plain,
( ~ para(u,v,u,v)
| ~ coll(u,u,w)
| cyclic(v,w,u,u) ),
inference(res,[status(thm),theory(equality)],[33,78]),
[iquote('0:Res:33.1,78.1')] ).
cnf(1755,plain,
eqangle(skc9,skc11,skc11,skc9,skc11,skc7,skc11,skc8),
inference(res,[status(thm),theory(equality)],[1179,54]),
[iquote('0:Res:1179.0,54.0')] ).
cnf(1763,plain,
eqangle(skc11,skc9,skc11,skc7,skc11,skc9,skc11,skc8),
inference(res,[status(thm),theory(equality)],[1202,53]),
[iquote('0:Res:1202.0,53.0')] ).
cnf(1802,plain,
eqangle(skc11,skc9,skc11,skc9,skc11,skc7,skc11,skc8),
inference(res,[status(thm),theory(equality)],[1755,53]),
[iquote('0:Res:1755.0,53.0')] ).
cnf(1965,plain,
( ~ para(skc11,skc7,skc11,skc8)
| para(skc11,skc9,skc11,skc9) ),
inference(res,[status(thm),theory(equality)],[1802,86]),
[iquote('0:Res:1802.0,86.1')] ).
cnf(1977,plain,
para(skc11,skc9,skc11,skc9),
inference(mrr,[status(thm)],[1965,730]),
[iquote('0:MRR:1965.0,730.0')] ).
cnf(3067,plain,
( ~ cyclic(skc9,skc7,skc11,skc9)
| ~ cyclic(skc9,skc7,skc11,skc8)
| ~ cyclic(skc9,skc7,skc11,skc11)
| cong(skc9,skc7,skc9,skc8) ),
inference(res,[status(thm),theory(equality)],[1763,120]),
[iquote('0:Res:1763.0,120.3')] ).
cnf(3079,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)],[34,120]),
[iquote('0:Res:34.1,120.3')] ).
cnf(3085,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)],[3079]),
[iquote('0:Obv:3079.0')] ).
cnf(3086,plain,
( ~ cyclic(u,v,w,u)
| ~ cyclic(u,v,w,v)
| cong(u,v,u,v) ),
inference(con,[status(thm)],[3085]),
[iquote('0:Con:3085.2')] ).
cnf(3852,plain,
( ~ para(u,v,u,v)
| coll(u,w,v)
| cyclic(v,v,u,w) ),
inference(res,[status(thm),theory(equality)],[1181,61]),
[iquote('0:Res:1181.1,61.0')] ).
cnf(3863,plain,
( ~ para(u,v,u,v)
| ~ coll(u,w,v)
| cyclic(v,v,u,w) ),
inference(res,[status(thm),theory(equality)],[1181,78]),
[iquote('0:Res:1181.1,78.1')] ).
cnf(3877,plain,
( ~ para(u,v,u,v)
| cyclic(v,v,u,w) ),
inference(mrr,[status(thm)],[3863,3852]),
[iquote('0:MRR:3863.1,3852.1')] ).
cnf(4117,plain,
( ~ para(u,v,u,v)
| para(w,x,w,x) ),
inference(res,[status(thm),theory(equality)],[1228,32]),
[iquote('0:Res:1228.1,32.0')] ).
cnf(10988,plain,
cyclic(skc9,skc9,skc11,u),
inference(res,[status(thm),theory(equality)],[1977,3877]),
[iquote('0:Res:1977.0,3877.0')] ).
cnf(11082,plain,
( ~ cyclic(skc9,skc9,skc11,u)
| cyclic(skc9,skc11,u,v) ),
inference(res,[status(thm),theory(equality)],[10988,46]),
[iquote('0:Res:10988.0,46.0')] ).
cnf(11099,plain,
cyclic(skc9,skc11,u,v),
inference(mrr,[status(thm)],[11082,10988]),
[iquote('0:MRR:11082.0,10988.0')] ).
cnf(11186,plain,
para(u,v,u,v),
inference(res,[status(thm),theory(equality)],[1977,4117]),
[iquote('0:Res:1977.0,4117.0')] ).
cnf(11197,plain,
( coll(u,u,v)
| cyclic(v,w,u,u) ),
inference(mrr,[status(thm)],[1094,11186]),
[iquote('0:MRR:1094.0,11186.0')] ).
cnf(11198,plain,
( ~ coll(u,u,v)
| cyclic(w,v,u,u) ),
inference(mrr,[status(thm)],[1476,11186]),
[iquote('0:MRR:1476.0,11186.0')] ).
cnf(11200,plain,
cyclic(u,u,v,w),
inference(mrr,[status(thm)],[3877,11186]),
[iquote('0:MRR:3877.0,11186.0')] ).
cnf(11378,plain,
( coll(u,u,v)
| cyclic(w,v,u,u) ),
inference(res,[status(thm),theory(equality)],[11197,20]),
[iquote('0:Res:11197.1,20.0')] ).
cnf(11383,plain,
cyclic(u,v,w,w),
inference(mrr,[status(thm)],[11378,11198]),
[iquote('0:MRR:11378.0,11198.0')] ).
cnf(11469,plain,
( ~ cyclic(skc9,skc7,skc11,skc9)
| ~ cyclic(skc9,skc7,skc11,skc8)
| cong(skc9,skc7,skc9,skc8) ),
inference(mrr,[status(thm)],[3067,11383]),
[iquote('0:MRR:3067.2,11383.0')] ).
cnf(11991,plain,
cyclic(skc9,u,skc11,v),
inference(res,[status(thm),theory(equality)],[11099,19]),
[iquote('0:Res:11099.0,19.0')] ).
cnf(12008,plain,
cong(skc9,skc7,skc9,skc8),
inference(mrr,[status(thm)],[11469,11991]),
[iquote('0:MRR:11469.1,11469.0,11991.0')] ).
cnf(12027,plain,
midp(skc9,skc7,skc8),
inference(mrr,[status(thm)],[121,12008]),
[iquote('0:MRR:121.0,12008.0')] ).
cnf(12742,plain,
( ~ cong(u,v,u,v)
| ~ cong(u,w,u,w)
| perp(w,u,u,v) ),
inference(res,[status(thm),theory(equality)],[11200,94]),
[iquote('0:Res:11200.0,94.0')] ).
cnf(12743,plain,
( ~ cyclic(u,u,v,w)
| cyclic(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[11200,46]),
[iquote('0:Res:11200.0,46.0')] ).
cnf(12811,plain,
cyclic(u,v,w,x),
inference(mrr,[status(thm)],[12743,11200]),
[iquote('0:MRR:12743.0,11200.0')] ).
cnf(12815,plain,
( ~ eqangle(u,v,u,w,x,y,x,z)
| cong(v,w,y,z) ),
inference(mrr,[status(thm)],[120,12811]),
[iquote('0:MRR:120.2,120.1,120.0,12811.0')] ).
cnf(12830,plain,
( ~ perp(u,v,v,w)
| circle(skf35(v,w,u),u,w,v) ),
inference(mrr,[status(thm)],[68,12811]),
[iquote('0:MRR:68.1,12811.0')] ).
cnf(12831,plain,
cong(u,v,u,v),
inference(mrr,[status(thm)],[3086,12811]),
[iquote('0:MRR:3086.1,3086.0,12811.0')] ).
cnf(13158,plain,
perp(u,v,v,w),
inference(mrr,[status(thm)],[12742,12831]),
[iquote('0:MRR:12742.0,12742.1,12831.0,12831.0')] ).
cnf(13172,plain,
( ~ circle(u,v,w,x)
| eqangle(v,y,v,w,x,v,x,w) ),
inference(mrr,[status(thm)],[91,13158]),
[iquote('0:MRR:91.0,13158.0')] ).
cnf(13175,plain,
( ~ midp(u,v,w)
| cong(v,u,x,u) ),
inference(mrr,[status(thm)],[39,13158]),
[iquote('0:MRR:39.1,13158.0')] ).
cnf(13182,plain,
circle(skf35(u,v,w),w,v,u),
inference(mrr,[status(thm)],[12830,13158]),
[iquote('0:MRR:12830.0,13158.0')] ).
cnf(13476,plain,
cong(skc7,skc9,u,skc9),
inference(res,[status(thm),theory(equality)],[12027,13175]),
[iquote('0:Res:12027.0,13175.0')] ).
cnf(16141,plain,
eqangle(u,v,u,w,x,u,x,w),
inference(res,[status(thm),theory(equality)],[13182,13172]),
[iquote('0:Res:13182.0,13172.0')] ).
cnf(16378,plain,
( ~ coll(skc7,skc9,skc9)
| midp(skc7,skc9,skc9) ),
inference(res,[status(thm),theory(equality)],[13476,38]),
[iquote('0:Res:13476.0,38.1')] ).
cnf(16385,plain,
midp(skc7,skc9,skc9),
inference(mrr,[status(thm)],[16378,549]),
[iquote('0:MRR:16378.0,549.0')] ).
cnf(16386,plain,
cong(skc9,skc7,u,skc7),
inference(res,[status(thm),theory(equality)],[16385,13175]),
[iquote('0:Res:16385.0,13175.0')] ).
cnf(16394,plain,
~ cong(skc9,skc8,skc10,skc8),
inference(mrr,[status(thm)],[201,16386]),
[iquote('0:MRR:201.1,16386.0')] ).
cnf(19303,plain,
cong(u,v,w,v),
inference(res,[status(thm),theory(equality)],[16141,12815]),
[iquote('0:Res:16141.0,12815.0')] ).
cnf(19323,plain,
$false,
inference(unc,[status(thm)],[19303,16394]),
[iquote('0:UnC:19303.0,16394.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO622+1 : TPTP v8.1.0. Released v7.5.0.
% 0.07/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n021.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 : Sat Jun 18 06:23:01 EDT 2022
% 0.12/0.33 % CPUTime :
% 11.09/11.36
% 11.09/11.36 SPASS V 3.9
% 11.09/11.36 SPASS beiseite: Proof found.
% 11.09/11.36 % SZS status Theorem
% 11.09/11.36 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.09/11.36 SPASS derived 17991 clauses, backtracked 0 clauses, performed 2 splits and kept 10027 clauses.
% 11.09/11.36 SPASS allocated 99076 KBytes.
% 11.09/11.36 SPASS spent 0:0:10.90 on the problem.
% 11.09/11.36 0:00:00.04 for the input.
% 11.09/11.36 0:00:00.24 for the FLOTTER CNF translation.
% 11.09/11.36 0:00:00.36 for inferences.
% 11.09/11.36 0:00:00.25 for the backtracking.
% 11.09/11.36 0:00:09.71 for the reduction.
% 11.09/11.36
% 11.09/11.36
% 11.09/11.36 Here is a proof with depth 8, length 92 :
% 11.09/11.36 % SZS output start Refutation
% See solution above
% 11.09/11.36 Formulae used in the proof : exemplo6GDDFULL8110985 ruleD1 ruleD2 ruleD5 ruleD15 ruleD16 ruleD3 ruleD39 ruleD40 ruleD41 ruleD67 ruleD52 ruleD17 ruleD56 ruleD18 ruleD19 ruleD20 ruleD21 ruleD42a ruleX14 ruleD42b ruleD73 ruleD48 ruleD57 ruleD43
% 11.09/11.36
%------------------------------------------------------------------------------