%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GRA002+2 : TPTP v8.1.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n029.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 07:22:08 EDT 2022
% Result : Theorem 35.44s 35.63s
% Output : Refutation 35.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 21
% Syntax : Number of clauses : 79 ( 23 unt; 21 nHn; 79 RR)
% Number of literals : 221 ( 0 equ; 136 neg)
% Maximal clause size : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 2 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
complete,
file('GRA002+2.p',unknown),
[] ).
cnf(2,axiom,
shortest_path(skc4,skc5,skc3),
file('GRA002+2.p',unknown),
[] ).
cnf(3,axiom,
edge(skf13(u,v)),
file('GRA002+2.p',unknown),
[] ).
cnf(8,axiom,
( ~ sequential(u,v)
| edge(u) ),
file('GRA002+2.p',unknown),
[] ).
cnf(9,axiom,
( ~ sequential(u,v)
| edge(v) ),
file('GRA002+2.p',unknown),
[] ).
cnf(13,axiom,
less_or_equal(number_of_in(u,v),number_of_in(u,graph)),
file('GRA002+2.p',unknown),
[] ).
cnf(19,axiom,
( ~ sequential(u,v)
| ~ equal(u,v) ),
file('GRA002+2.p',unknown),
[] ).
cnf(21,axiom,
~ less_or_equal(minus(length_of(skc3),n1),number_of_in(triangles,graph)),
file('GRA002+2.p',unknown),
[] ).
cnf(27,axiom,
( ~ shortest_path(u,v,w)
| path(u,v,w) ),
file('GRA002+2.p',unknown),
[] ).
cnf(31,axiom,
( ~ on_path(u,v)
| ~ path(w,x,v)
| edge(u) ),
file('GRA002+2.p',unknown),
[] ).
cnf(34,axiom,
( ~ path(u,v,w)
| equal(minus(length_of(w),n1),number_of_in(sequential_pairs,w)) ),
file('GRA002+2.p',unknown),
[] ).
cnf(43,axiom,
( ~ shortest_path(u,v,w)
| ~ precedes(x,y,w)
| ~ precedes(y,x,w) ),
file('GRA002+2.p',unknown),
[] ).
cnf(44,axiom,
( ~ path(u,v,w)
| on_path(skf12(w),w)
| equal(number_of_in(triangles,w),number_of_in(sequential_pairs,w)) ),
file('GRA002+2.p',unknown),
[] ).
cnf(45,axiom,
( ~ path(u,v,w)
| on_path(skf10(w),w)
| equal(number_of_in(triangles,w),number_of_in(sequential_pairs,w)) ),
file('GRA002+2.p',unknown),
[] ).
cnf(46,axiom,
( ~ path(u,v,w)
| sequential(skf12(w),skf10(w))
| equal(number_of_in(triangles,w),number_of_in(sequential_pairs,w)) ),
file('GRA002+2.p',unknown),
[] ).
cnf(48,axiom,
( ~ edge(u)
| ~ edge(v)
| ~ equal(head_of(u),tail_of(v))
| sequential(u,v)
| equal(u,v) ),
file('GRA002+2.p',unknown),
[] ).
cnf(50,axiom,
( ~ path(u,v,w)
| ~ triangle(skf12(w),skf10(w),x)
| equal(number_of_in(triangles,w),number_of_in(sequential_pairs,w)) ),
file('GRA002+2.p',unknown),
[] ).
cnf(51,axiom,
( ~ complete
| ~ precedes(u,v,w)
| ~ shortest_path(x,y,w)
| equal(tail_of(skf13(u,v)),head_of(v)) ),
file('GRA002+2.p',unknown),
[] ).
cnf(52,axiom,
( ~ complete
| ~ precedes(u,v,w)
| ~ shortest_path(x,y,w)
| equal(head_of(skf13(u,v)),tail_of(u)) ),
file('GRA002+2.p',unknown),
[] ).
cnf(57,axiom,
( ~ on_path(u,v)
| ~ on_path(w,v)
| ~ sequential(w,u)
| ~ path(x,y,v)
| precedes(w,u,v) ),
file('GRA002+2.p',unknown),
[] ).
cnf(64,axiom,
( ~ edge(u)
| ~ edge(v)
| ~ edge(w)
| ~ sequential(w,v)
| ~ sequential(v,u)
| ~ sequential(u,w)
| triangle(w,v,u) ),
file('GRA002+2.p',unknown),
[] ).
cnf(70,plain,
( ~ shortest_path(u,v,w)
| ~ precedes(x,y,w)
| equal(head_of(skf13(x,y)),tail_of(x)) ),
inference(mrr,[status(thm)],[52,1]),
[iquote('0:MRR:52.0,1.0')] ).
cnf(71,plain,
( ~ shortest_path(u,v,w)
| ~ precedes(x,y,w)
| equal(tail_of(skf13(x,y)),head_of(y)) ),
inference(mrr,[status(thm)],[51,1]),
[iquote('0:MRR:51.0,1.0')] ).
cnf(74,plain,
( ~ sequential(u,v)
| ~ sequential(w,u)
| ~ sequential(v,w)
| triangle(v,w,u) ),
inference(mrr,[status(thm)],[64,8]),
[iquote('0:MRR:64.0,64.1,64.2,8.1,8.1,8.1')] ).
cnf(78,plain,
path(skc4,skc5,skc3),
inference(res,[status(thm),theory(equality)],[2,27]),
[iquote('0:Res:2.0,27.0')] ).
cnf(80,plain,
( ~ precedes(u,v,skc3)
| equal(tail_of(skf13(u,v)),head_of(v)) ),
inference(res,[status(thm),theory(equality)],[2,71]),
[iquote('0:Res:2.0,71.1')] ).
cnf(81,plain,
( ~ precedes(u,v,skc3)
| equal(head_of(skf13(u,v)),tail_of(u)) ),
inference(res,[status(thm),theory(equality)],[2,70]),
[iquote('0:Res:2.0,70.1')] ).
cnf(82,plain,
( ~ precedes(u,v,skc3)
| ~ precedes(v,u,skc3) ),
inference(res,[status(thm),theory(equality)],[2,43]),
[iquote('0:Res:2.0,43.2')] ).
cnf(97,plain,
( ~ on_path(u,skc3)
| edge(u) ),
inference(res,[status(thm),theory(equality)],[78,31]),
[iquote('0:Res:78.0,31.1')] ).
cnf(109,plain,
equal(minus(length_of(skc3),n1),number_of_in(sequential_pairs,skc3)),
inference(res,[status(thm),theory(equality)],[78,34]),
[iquote('0:Res:78.0,34.0')] ).
cnf(110,plain,
~ less_or_equal(number_of_in(sequential_pairs,skc3),number_of_in(triangles,graph)),
inference(rew,[status(thm),theory(equality)],[109,21]),
[iquote('0:Rew:109.0,21.0')] ).
cnf(126,plain,
( on_path(skf10(skc3),skc3)
| equal(number_of_in(triangles,skc3),number_of_in(sequential_pairs,skc3)) ),
inference(res,[status(thm),theory(equality)],[78,45]),
[iquote('0:Res:78.0,45.0')] ).
cnf(127,plain,
( equal(number_of_in(triangles,skc3),number_of_in(sequential_pairs,skc3))
| edge(skf10(skc3)) ),
inference(res,[status(thm),theory(equality)],[126,97]),
[iquote('0:Res:126.0,97.0')] ).
cnf(128,plain,
( edge(skf10(skc3))
| less_or_equal(number_of_in(sequential_pairs,skc3),number_of_in(triangles,graph)) ),
inference(spr,[status(thm),theory(equality)],[127,13]),
[iquote('0:SpR:127.0,13.0')] ).
cnf(130,plain,
edge(skf10(skc3)),
inference(mrr,[status(thm)],[128,110]),
[iquote('0:MRR:128.1,110.0')] ).
cnf(131,plain,
( on_path(skf12(skc3),skc3)
| equal(number_of_in(triangles,skc3),number_of_in(sequential_pairs,skc3)) ),
inference(res,[status(thm),theory(equality)],[78,44]),
[iquote('0:Res:78.0,44.0')] ).
cnf(138,plain,
( equal(number_of_in(triangles,skc3),number_of_in(sequential_pairs,skc3))
| edge(skf12(skc3)) ),
inference(res,[status(thm),theory(equality)],[131,97]),
[iquote('0:Res:131.0,97.0')] ).
cnf(139,plain,
equal(number_of_in(triangles,skc3),number_of_in(sequential_pairs,skc3)),
inference(spt,[spt(split,[position(s1)])],[138]),
[iquote('1:Spt:138.0')] ).
cnf(140,plain,
less_or_equal(number_of_in(sequential_pairs,skc3),number_of_in(triangles,graph)),
inference(spr,[status(thm),theory(equality)],[139,13]),
[iquote('1:SpR:139.0,13.0')] ).
cnf(142,plain,
$false,
inference(mrr,[status(thm)],[140,110]),
[iquote('1:MRR:140.0,110.0')] ).
cnf(143,plain,
~ equal(number_of_in(triangles,skc3),number_of_in(sequential_pairs,skc3)),
inference(spt,[spt(split,[position(sa)])],[142,139]),
[iquote('1:Spt:142.0,138.0,139.0')] ).
cnf(144,plain,
edge(skf12(skc3)),
inference(spt,[spt(split,[position(s2)])],[138]),
[iquote('1:Spt:142.0,138.1')] ).
cnf(145,plain,
on_path(skf10(skc3),skc3),
inference(mrr,[status(thm)],[126,143]),
[iquote('1:MRR:126.1,143.0')] ).
cnf(146,plain,
on_path(skf12(skc3),skc3),
inference(mrr,[status(thm)],[131,143]),
[iquote('1:MRR:131.1,143.0')] ).
cnf(153,plain,
( sequential(skf12(skc3),skf10(skc3))
| equal(number_of_in(triangles,skc3),number_of_in(sequential_pairs,skc3)) ),
inference(res,[status(thm),theory(equality)],[78,46]),
[iquote('0:Res:78.0,46.0')] ).
cnf(154,plain,
sequential(skf12(skc3),skf10(skc3)),
inference(mrr,[status(thm)],[153,143]),
[iquote('1:MRR:153.1,143.0')] ).
cnf(156,plain,
~ equal(skf12(skc3),skf10(skc3)),
inference(res,[status(thm),theory(equality)],[154,19]),
[iquote('1:Res:154.0,19.0')] ).
cnf(181,plain,
( ~ sequential(u,skf12(v))
| ~ sequential(skf10(v),u)
| ~ sequential(skf12(v),skf10(v))
| ~ path(w,x,v)
| equal(number_of_in(triangles,v),number_of_in(sequential_pairs,v)) ),
inference(res,[status(thm),theory(equality)],[74,50]),
[iquote('0:Res:74.3,50.1')] ).
cnf(182,plain,
( ~ sequential(u,skf12(v))
| ~ sequential(skf10(v),u)
| ~ path(w,x,v)
| equal(number_of_in(triangles,v),number_of_in(sequential_pairs,v)) ),
inference(mrr,[status(thm)],[181,46]),
[iquote('0:MRR:181.2,46.1')] ).
cnf(322,plain,
( ~ on_path(u,skc3)
| ~ on_path(v,skc3)
| ~ sequential(v,u)
| precedes(v,u,skc3) ),
inference(res,[status(thm),theory(equality)],[78,57]),
[iquote('0:Res:78.0,57.3')] ).
cnf(327,plain,
( ~ on_path(u,skc3)
| ~ on_path(v,skc3)
| ~ sequential(v,u)
| ~ precedes(u,v,skc3) ),
inference(res,[status(thm),theory(equality)],[322,82]),
[iquote('0:Res:322.3,82.0')] ).
cnf(337,plain,
( ~ on_path(u,skc3)
| ~ on_path(v,skc3)
| ~ sequential(v,u)
| ~ on_path(v,skc3)
| ~ on_path(u,skc3)
| ~ sequential(u,v) ),
inference(res,[status(thm),theory(equality)],[322,327]),
[iquote('0:Res:322.3,327.3')] ).
cnf(338,plain,
( ~ sequential(u,v)
| ~ on_path(u,skc3)
| ~ on_path(v,skc3)
| ~ sequential(v,u) ),
inference(obv,[status(thm),theory(equality)],[337]),
[iquote('0:Obv:337.1')] ).
cnf(340,plain,
( ~ on_path(skf12(skc3),skc3)
| ~ on_path(skf10(skc3),skc3)
| ~ sequential(skf10(skc3),skf12(skc3)) ),
inference(res,[status(thm),theory(equality)],[154,338]),
[iquote('1:Res:154.0,338.0')] ).
cnf(341,plain,
~ sequential(skf10(skc3),skf12(skc3)),
inference(mrr,[status(thm)],[340,146,145]),
[iquote('1:MRR:340.0,340.1,146.0,145.0')] ).
cnf(342,plain,
( ~ edge(skf10(skc3))
| ~ edge(skf12(skc3))
| ~ equal(head_of(skf10(skc3)),tail_of(skf12(skc3)))
| equal(skf12(skc3),skf10(skc3)) ),
inference(res,[status(thm),theory(equality)],[48,341]),
[iquote('1:Res:48.3,341.0')] ).
cnf(343,plain,
( ~ equal(head_of(skf10(skc3)),tail_of(skf12(skc3)))
| equal(skf12(skc3),skf10(skc3)) ),
inference(ssi,[status(thm)],[342,144,130]),
[iquote('1:SSi:342.1,342.0,144.0,130.0')] ).
cnf(344,plain,
~ equal(head_of(skf10(skc3)),tail_of(skf12(skc3))),
inference(mrr,[status(thm)],[343,156]),
[iquote('1:MRR:343.1,156.0')] ).
cnf(527,plain,
( ~ edge(u)
| ~ edge(skf12(v))
| ~ equal(head_of(u),tail_of(skf12(v)))
| ~ sequential(skf10(v),u)
| ~ path(w,x,v)
| equal(u,skf12(v))
| equal(number_of_in(triangles,v),number_of_in(sequential_pairs,v)) ),
inference(res,[status(thm),theory(equality)],[48,182]),
[iquote('0:Res:48.3,182.0')] ).
cnf(528,plain,
( ~ edge(skf12(u))
| ~ equal(head_of(v),tail_of(skf12(u)))
| ~ sequential(skf10(u),v)
| ~ path(w,x,u)
| equal(v,skf12(u))
| equal(number_of_in(triangles,u),number_of_in(sequential_pairs,u)) ),
inference(mrr,[status(thm)],[527,9]),
[iquote('0:MRR:527.0,9.1')] ).
cnf(1656,plain,
( ~ equal(head_of(u),tail_of(skf12(skc3)))
| ~ sequential(skf10(skc3),u)
| ~ path(v,w,skc3)
| equal(u,skf12(skc3))
| equal(number_of_in(triangles,skc3),number_of_in(sequential_pairs,skc3)) ),
inference(sor,[status(thm)],[528,144]),
[iquote('1:SoR:528.0,144.0')] ).
cnf(1657,plain,
( ~ equal(head_of(u),tail_of(skf12(skc3)))
| ~ sequential(skf10(skc3),u)
| ~ path(v,w,skc3)
| equal(u,skf12(skc3)) ),
inference(mrr,[status(thm)],[1656,143]),
[iquote('1:MRR:1656.4,143.0')] ).
cnf(1658,plain,
( ~ precedes(u,v,skc3)
| ~ equal(tail_of(u),tail_of(skf12(skc3)))
| ~ sequential(skf10(skc3),skf13(u,v))
| ~ path(w,x,skc3)
| equal(skf13(u,v),skf12(skc3)) ),
inference(spl,[status(thm),theory(equality)],[81,1657]),
[iquote('1:SpL:81.1,1657.0')] ).
cnf(8005,plain,
( ~ precedes(skf12(skc3),u,skc3)
| ~ sequential(skf10(skc3),skf13(skf12(skc3),u))
| ~ path(v,w,skc3)
| equal(skf13(skf12(skc3),u),skf12(skc3)) ),
inference(eqr,[status(thm),theory(equality)],[1658]),
[iquote('1:EqR:1658.1')] ).
cnf(8018,plain,
( ~ edge(skf10(skc3))
| ~ edge(skf13(skf12(skc3),u))
| ~ equal(tail_of(skf13(skf12(skc3),u)),head_of(skf10(skc3)))
| ~ precedes(skf12(skc3),u,skc3)
| ~ path(v,w,skc3)
| equal(skf13(skf12(skc3),u),skf10(skc3))
| equal(skf13(skf12(skc3),u),skf12(skc3)) ),
inference(res,[status(thm),theory(equality)],[48,8005]),
[iquote('1:Res:48.3,8005.1')] ).
cnf(8019,plain,
( ~ edge(skf10(skc3))
| ~ edge(skf13(skf12(skc3),u))
| ~ equal(head_of(u),head_of(skf10(skc3)))
| ~ precedes(skf12(skc3),u,skc3)
| ~ path(v,w,skc3)
| equal(skf13(skf12(skc3),u),skf10(skc3))
| equal(skf13(skf12(skc3),u),skf12(skc3)) ),
inference(rew,[status(thm),theory(equality)],[80,8018]),
[iquote('1:Rew:80.1,8018.2')] ).
cnf(8020,plain,
( ~ equal(head_of(u),head_of(skf10(skc3)))
| ~ precedes(skf12(skc3),u,skc3)
| ~ path(v,w,skc3)
| equal(skf13(skf12(skc3),u),skf10(skc3))
| equal(skf13(skf12(skc3),u),skf12(skc3)) ),
inference(ssi,[status(thm)],[8019,3,144,130]),
[iquote('1:SSi:8019.1,8019.0,3.0,144.0,130.0')] ).
cnf(11767,plain,
( ~ precedes(skf12(skc3),skf10(skc3),skc3)
| ~ path(u,v,skc3)
| equal(skf13(skf12(skc3),skf10(skc3)),skf10(skc3))
| equal(skf13(skf12(skc3),skf10(skc3)),skf12(skc3)) ),
inference(eqr,[status(thm),theory(equality)],[8020]),
[iquote('1:EqR:8020.0')] ).
cnf(11785,plain,
( ~ on_path(skf10(skc3),skc3)
| ~ on_path(skf12(skc3),skc3)
| ~ sequential(skf12(skc3),skf10(skc3))
| ~ path(u,v,skc3)
| equal(skf13(skf12(skc3),skf10(skc3)),skf10(skc3))
| equal(skf13(skf12(skc3),skf10(skc3)),skf12(skc3)) ),
inference(res,[status(thm),theory(equality)],[322,11767]),
[iquote('1:Res:322.3,11767.0')] ).
cnf(11788,plain,
( ~ path(u,v,skc3)
| equal(skf13(skf12(skc3),skf10(skc3)),skf10(skc3))
| equal(skf13(skf12(skc3),skf10(skc3)),skf12(skc3)) ),
inference(mrr,[status(thm)],[11785,145,146,154]),
[iquote('1:MRR:11785.0,11785.1,11785.2,145.0,146.0,154.0')] ).
cnf(11790,plain,
( equal(skf13(skf12(skc3),skf10(skc3)),skf10(skc3))
| equal(skf13(skf12(skc3),skf10(skc3)),skf12(skc3)) ),
inference(res,[status(thm),theory(equality)],[78,11788]),
[iquote('1:Res:78.0,11788.0')] ).
cnf(11798,plain,
( ~ precedes(skf12(skc3),skf10(skc3),skc3)
| equal(skf13(skf12(skc3),skf10(skc3)),skf10(skc3))
| equal(head_of(skf10(skc3)),tail_of(skf12(skc3))) ),
inference(spr,[status(thm),theory(equality)],[11790,80]),
[iquote('1:SpR:11790.1,80.1')] ).
cnf(11867,plain,
( ~ precedes(skf12(skc3),skf10(skc3),skc3)
| equal(skf13(skf12(skc3),skf10(skc3)),skf10(skc3)) ),
inference(mrr,[status(thm)],[11798,344]),
[iquote('1:MRR:11798.2,344.0')] ).
cnf(11869,plain,
( ~ on_path(skf10(skc3),skc3)
| ~ on_path(skf12(skc3),skc3)
| ~ sequential(skf12(skc3),skf10(skc3))
| equal(skf13(skf12(skc3),skf10(skc3)),skf10(skc3)) ),
inference(res,[status(thm),theory(equality)],[322,11867]),
[iquote('1:Res:322.3,11867.0')] ).
cnf(11872,plain,
equal(skf13(skf12(skc3),skf10(skc3)),skf10(skc3)),
inference(mrr,[status(thm)],[11869,145,146,154]),
[iquote('1:MRR:11869.0,11869.1,11869.2,145.0,146.0,154.0')] ).
cnf(11876,plain,
( ~ precedes(skf12(skc3),skf10(skc3),skc3)
| equal(head_of(skf10(skc3)),tail_of(skf12(skc3))) ),
inference(spr,[status(thm),theory(equality)],[11872,81]),
[iquote('1:SpR:11872.0,81.1')] ).
cnf(11946,plain,
~ precedes(skf12(skc3),skf10(skc3),skc3),
inference(mrr,[status(thm)],[11876,344]),
[iquote('1:MRR:11876.1,344.0')] ).
cnf(11948,plain,
( ~ on_path(skf10(skc3),skc3)
| ~ on_path(skf12(skc3),skc3)
| ~ sequential(skf12(skc3),skf10(skc3)) ),
inference(res,[status(thm),theory(equality)],[322,11946]),
[iquote('1:Res:322.3,11946.0')] ).
cnf(11951,plain,
$false,
inference(mrr,[status(thm)],[11948,145,146,154]),
[iquote('1:MRR:11948.0,11948.1,11948.2,145.0,146.0,154.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRA002+2 : TPTP v8.1.0. Bugfixed v3.2.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n029.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Tue May 31 01:34:44 EDT 2022
% 0.12/0.34 % CPUTime :
% 35.44/35.63
% 35.44/35.63 SPASS V 3.9
% 35.44/35.63 SPASS beiseite: Proof found.
% 35.44/35.63 % SZS status Theorem
% 35.44/35.63 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 35.44/35.63 SPASS derived 7777 clauses, backtracked 41 clauses, performed 10 splits and kept 5393 clauses.
% 35.44/35.63 SPASS allocated 112882 KBytes.
% 35.44/35.63 SPASS spent 0:0:35.27 on the problem.
% 35.44/35.63 0:00:00.04 for the input.
% 35.44/35.63 0:00:00.07 for the FLOTTER CNF translation.
% 35.44/35.63 0:00:00.31 for inferences.
% 35.44/35.63 0:00:00.75 for the backtracking.
% 35.44/35.63 0:0:33.97 for the reduction.
% 35.44/35.63
% 35.44/35.63
% 35.44/35.63 Here is a proof with depth 15, length 79 :
% 35.44/35.63 % SZS output start Refutation
% See solution above
% 35.74/35.94 Formulae used in the proof : maximal_path_length back_edge shortest_path_defn path_properties sequential_defn graph_has_them_all on_path_properties path_length_sequential_pairs shortest_path_properties sequential_pairs_and_triangles precedes_defn triangle_defn
% 35.74/35.94
%------------------------------------------------------------------------------