%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV558-1.007 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n023.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 : Wed Jul 20 21:44:15 EDT 2022
% Result : Unsatisfiable 0.19s 0.44s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 32
% Syntax : Number of clauses : 110 ( 110 unt; 0 nHn; 110 RR)
% Number of literals : 110 ( 0 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 42 ( 42 usr; 40 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(select(store(u,v,w),v),w),
file('SWV558-1.007.p',unknown),
[] ).
cnf(3,axiom,
equal(store(u,v,select(u,v)),u),
file('SWV558-1.007.p',unknown),
[] ).
cnf(6,axiom,
equal(store(a1,i1,e_28),a_29),
file('SWV558-1.007.p',unknown),
[] ).
cnf(7,axiom,
equal(store(a2,i1,e_30),a_31),
file('SWV558-1.007.p',unknown),
[] ).
cnf(8,axiom,
equal(store(a_29,i2,e_32),a_33),
file('SWV558-1.007.p',unknown),
[] ).
cnf(9,axiom,
equal(store(a_31,i2,e_34),a_35),
file('SWV558-1.007.p',unknown),
[] ).
cnf(10,axiom,
equal(store(a_33,i3,e_36),a_37),
file('SWV558-1.007.p',unknown),
[] ).
cnf(11,axiom,
equal(store(a_35,i3,e_38),a_39),
file('SWV558-1.007.p',unknown),
[] ).
cnf(12,axiom,
equal(store(a_37,i4,e_40),a_41),
file('SWV558-1.007.p',unknown),
[] ).
cnf(13,axiom,
equal(store(a_39,i4,e_42),a_43),
file('SWV558-1.007.p',unknown),
[] ).
cnf(14,axiom,
equal(store(a_41,i5,e_44),a_45),
file('SWV558-1.007.p',unknown),
[] ).
cnf(15,axiom,
equal(store(a_43,i5,e_46),a_47),
file('SWV558-1.007.p',unknown),
[] ).
cnf(16,axiom,
equal(store(a_45,i6,e_48),a_49),
file('SWV558-1.007.p',unknown),
[] ).
cnf(17,axiom,
equal(store(a_47,i6,e_50),a_51),
file('SWV558-1.007.p',unknown),
[] ).
cnf(18,axiom,
equal(store(a_49,i7,e_52),a_53),
file('SWV558-1.007.p',unknown),
[] ).
cnf(19,axiom,
equal(store(a_51,i7,e_54),a_55),
file('SWV558-1.007.p',unknown),
[] ).
cnf(20,axiom,
equal(select(a2,i1),e_28),
file('SWV558-1.007.p',unknown),
[] ).
cnf(21,axiom,
equal(select(a1,i1),e_30),
file('SWV558-1.007.p',unknown),
[] ).
cnf(22,axiom,
equal(select(a_31,i2),e_32),
file('SWV558-1.007.p',unknown),
[] ).
cnf(23,axiom,
equal(select(a_29,i2),e_34),
file('SWV558-1.007.p',unknown),
[] ).
cnf(24,axiom,
equal(select(a_35,i3),e_36),
file('SWV558-1.007.p',unknown),
[] ).
cnf(25,axiom,
equal(select(a_33,i3),e_38),
file('SWV558-1.007.p',unknown),
[] ).
cnf(26,axiom,
equal(select(a_39,i4),e_40),
file('SWV558-1.007.p',unknown),
[] ).
cnf(27,axiom,
equal(select(a_37,i4),e_42),
file('SWV558-1.007.p',unknown),
[] ).
cnf(28,axiom,
equal(select(a_43,i5),e_44),
file('SWV558-1.007.p',unknown),
[] ).
cnf(29,axiom,
equal(select(a_41,i5),e_46),
file('SWV558-1.007.p',unknown),
[] ).
cnf(30,axiom,
equal(select(a_47,i6),e_48),
file('SWV558-1.007.p',unknown),
[] ).
cnf(31,axiom,
equal(select(a_45,i6),e_50),
file('SWV558-1.007.p',unknown),
[] ).
cnf(32,axiom,
equal(select(a_51,i7),e_52),
file('SWV558-1.007.p',unknown),
[] ).
cnf(33,axiom,
equal(select(a_49,i7),e_54),
file('SWV558-1.007.p',unknown),
[] ).
cnf(34,axiom,
equal(a_55,a_53),
file('SWV558-1.007.p',unknown),
[] ).
cnf(35,axiom,
~ equal(a2,a1),
file('SWV558-1.007.p',unknown),
[] ).
cnf(36,plain,
equal(store(a_51,i7,e_54),a_53),
inference(rew,[status(thm),theory(equality)],[34,19]),
[iquote('0:Rew:34.0,19.0')] ).
cnf(71,plain,
equal(store(a_49,i7,e_54),a_49),
inference(spr,[status(thm),theory(equality)],[33,3]),
[iquote('0:SpR:33.0,3.0')] ).
cnf(72,plain,
equal(store(a_51,i7,e_52),a_51),
inference(spr,[status(thm),theory(equality)],[32,3]),
[iquote('0:SpR:32.0,3.0')] ).
cnf(73,plain,
equal(store(a_45,i6,e_50),a_45),
inference(spr,[status(thm),theory(equality)],[31,3]),
[iquote('0:SpR:31.0,3.0')] ).
cnf(74,plain,
equal(store(a_47,i6,e_48),a_47),
inference(spr,[status(thm),theory(equality)],[30,3]),
[iquote('0:SpR:30.0,3.0')] ).
cnf(75,plain,
equal(store(a_41,i5,e_46),a_41),
inference(spr,[status(thm),theory(equality)],[29,3]),
[iquote('0:SpR:29.0,3.0')] ).
cnf(76,plain,
equal(store(a_43,i5,e_44),a_43),
inference(spr,[status(thm),theory(equality)],[28,3]),
[iquote('0:SpR:28.0,3.0')] ).
cnf(77,plain,
equal(store(a_37,i4,e_42),a_37),
inference(spr,[status(thm),theory(equality)],[27,3]),
[iquote('0:SpR:27.0,3.0')] ).
cnf(78,plain,
equal(store(a_39,i4,e_40),a_39),
inference(spr,[status(thm),theory(equality)],[26,3]),
[iquote('0:SpR:26.0,3.0')] ).
cnf(79,plain,
equal(store(a_33,i3,e_38),a_33),
inference(spr,[status(thm),theory(equality)],[25,3]),
[iquote('0:SpR:25.0,3.0')] ).
cnf(80,plain,
equal(store(a_35,i3,e_36),a_35),
inference(spr,[status(thm),theory(equality)],[24,3]),
[iquote('0:SpR:24.0,3.0')] ).
cnf(81,plain,
equal(store(a_29,i2,e_34),a_29),
inference(spr,[status(thm),theory(equality)],[23,3]),
[iquote('0:SpR:23.0,3.0')] ).
cnf(82,plain,
equal(store(a_31,i2,e_32),a_31),
inference(spr,[status(thm),theory(equality)],[22,3]),
[iquote('0:SpR:22.0,3.0')] ).
cnf(83,plain,
equal(store(a1,i1,e_30),a1),
inference(spr,[status(thm),theory(equality)],[21,3]),
[iquote('0:SpR:21.0,3.0')] ).
cnf(84,plain,
equal(store(a2,i1,e_28),a2),
inference(spr,[status(thm),theory(equality)],[20,3]),
[iquote('0:SpR:20.0,3.0')] ).
cnf(90,plain,
equal(select(a_53,i7),e_54),
inference(spr,[status(thm),theory(equality)],[36,1]),
[iquote('0:SpR:36.0,1.0')] ).
cnf(92,plain,
equal(select(a_53,i7),e_52),
inference(spr,[status(thm),theory(equality)],[18,1]),
[iquote('0:SpR:18.0,1.0')] ).
cnf(94,plain,
equal(select(a_51,i6),e_50),
inference(spr,[status(thm),theory(equality)],[17,1]),
[iquote('0:SpR:17.0,1.0')] ).
cnf(95,plain,
equal(select(a_49,i6),e_48),
inference(spr,[status(thm),theory(equality)],[16,1]),
[iquote('0:SpR:16.0,1.0')] ).
cnf(97,plain,
equal(select(a_47,i5),e_46),
inference(spr,[status(thm),theory(equality)],[15,1]),
[iquote('0:SpR:15.0,1.0')] ).
cnf(98,plain,
equal(select(a_45,i5),e_44),
inference(spr,[status(thm),theory(equality)],[14,1]),
[iquote('0:SpR:14.0,1.0')] ).
cnf(99,plain,
equal(select(a_43,i4),e_42),
inference(spr,[status(thm),theory(equality)],[13,1]),
[iquote('0:SpR:13.0,1.0')] ).
cnf(100,plain,
equal(select(a_41,i4),e_40),
inference(spr,[status(thm),theory(equality)],[12,1]),
[iquote('0:SpR:12.0,1.0')] ).
cnf(101,plain,
equal(select(a_39,i3),e_38),
inference(spr,[status(thm),theory(equality)],[11,1]),
[iquote('0:SpR:11.0,1.0')] ).
cnf(102,plain,
equal(select(a_37,i3),e_36),
inference(spr,[status(thm),theory(equality)],[10,1]),
[iquote('0:SpR:10.0,1.0')] ).
cnf(103,plain,
equal(select(a_35,i2),e_34),
inference(spr,[status(thm),theory(equality)],[9,1]),
[iquote('0:SpR:9.0,1.0')] ).
cnf(104,plain,
equal(select(a_33,i2),e_32),
inference(spr,[status(thm),theory(equality)],[8,1]),
[iquote('0:SpR:8.0,1.0')] ).
cnf(105,plain,
equal(select(a_31,i1),e_30),
inference(spr,[status(thm),theory(equality)],[7,1]),
[iquote('0:SpR:7.0,1.0')] ).
cnf(106,plain,
equal(select(a_29,i1),e_28),
inference(spr,[status(thm),theory(equality)],[6,1]),
[iquote('0:SpR:6.0,1.0')] ).
cnf(108,plain,
equal(e_54,e_52),
inference(rew,[status(thm),theory(equality)],[90,92]),
[iquote('0:Rew:90.0,92.0')] ).
cnf(110,plain,
equal(store(a_51,i7,e_52),a_53),
inference(rew,[status(thm),theory(equality)],[108,36]),
[iquote('0:Rew:108.0,36.0')] ).
cnf(111,plain,
equal(store(a_49,i7,e_52),a_49),
inference(rew,[status(thm),theory(equality)],[108,71]),
[iquote('0:Rew:108.0,71.0')] ).
cnf(114,plain,
equal(a_53,a_51),
inference(rew,[status(thm),theory(equality)],[72,110]),
[iquote('0:Rew:72.0,110.0')] ).
cnf(116,plain,
equal(store(a_49,i7,e_52),a_51),
inference(rew,[status(thm),theory(equality)],[114,18]),
[iquote('0:Rew:114.0,18.0')] ).
cnf(118,plain,
equal(a_51,a_49),
inference(rew,[status(thm),theory(equality)],[111,116]),
[iquote('0:Rew:111.0,116.0')] ).
cnf(120,plain,
equal(store(a_47,i6,e_50),a_49),
inference(rew,[status(thm),theory(equality)],[118,17]),
[iquote('0:Rew:118.0,17.0')] ).
cnf(122,plain,
equal(select(a_49,i6),e_50),
inference(rew,[status(thm),theory(equality)],[118,94]),
[iquote('0:Rew:118.0,94.0')] ).
cnf(125,plain,
equal(e_50,e_48),
inference(rew,[status(thm),theory(equality)],[95,122]),
[iquote('0:Rew:95.0,122.0')] ).
cnf(127,plain,
equal(store(a_45,i6,e_48),a_45),
inference(rew,[status(thm),theory(equality)],[125,73]),
[iquote('0:Rew:125.0,73.0')] ).
cnf(128,plain,
equal(a_49,a_47),
inference(rew,[status(thm),theory(equality)],[74,120,125]),
[iquote('0:Rew:74.0,120.0,125.0,120.0')] ).
cnf(129,plain,
equal(store(a_45,i6,e_48),a_47),
inference(rew,[status(thm),theory(equality)],[128,16]),
[iquote('0:Rew:128.0,16.0')] ).
cnf(137,plain,
equal(a_47,a_45),
inference(rew,[status(thm),theory(equality)],[127,129]),
[iquote('0:Rew:127.0,129.0')] ).
cnf(139,plain,
equal(store(a_43,i5,e_46),a_45),
inference(rew,[status(thm),theory(equality)],[137,15]),
[iquote('0:Rew:137.0,15.0')] ).
cnf(141,plain,
equal(select(a_45,i5),e_46),
inference(rew,[status(thm),theory(equality)],[137,97]),
[iquote('0:Rew:137.0,97.0')] ).
cnf(148,plain,
equal(e_46,e_44),
inference(rew,[status(thm),theory(equality)],[98,141]),
[iquote('0:Rew:98.0,141.0')] ).
cnf(150,plain,
equal(store(a_41,i5,e_44),a_41),
inference(rew,[status(thm),theory(equality)],[148,75]),
[iquote('0:Rew:148.0,75.0')] ).
cnf(152,plain,
equal(a_45,a_43),
inference(rew,[status(thm),theory(equality)],[76,139,148]),
[iquote('0:Rew:76.0,139.0,148.0,139.0')] ).
cnf(153,plain,
equal(store(a_41,i5,e_44),a_43),
inference(rew,[status(thm),theory(equality)],[152,14]),
[iquote('0:Rew:152.0,14.0')] ).
cnf(166,plain,
equal(a_43,a_41),
inference(rew,[status(thm),theory(equality)],[150,153]),
[iquote('0:Rew:150.0,153.0')] ).
cnf(168,plain,
equal(store(a_39,i4,e_42),a_41),
inference(rew,[status(thm),theory(equality)],[166,13]),
[iquote('0:Rew:166.0,13.0')] ).
cnf(170,plain,
equal(select(a_41,i4),e_42),
inference(rew,[status(thm),theory(equality)],[166,99]),
[iquote('0:Rew:166.0,99.0')] ).
cnf(181,plain,
equal(e_42,e_40),
inference(rew,[status(thm),theory(equality)],[100,170]),
[iquote('0:Rew:100.0,170.0')] ).
cnf(183,plain,
equal(store(a_37,i4,e_40),a_37),
inference(rew,[status(thm),theory(equality)],[181,77]),
[iquote('0:Rew:181.0,77.0')] ).
cnf(186,plain,
equal(a_41,a_39),
inference(rew,[status(thm),theory(equality)],[78,168,181]),
[iquote('0:Rew:78.0,168.0,181.0,168.0')] ).
cnf(187,plain,
equal(store(a_37,i4,e_40),a_39),
inference(rew,[status(thm),theory(equality)],[186,12]),
[iquote('0:Rew:186.0,12.0')] ).
cnf(205,plain,
equal(a_39,a_37),
inference(rew,[status(thm),theory(equality)],[183,187]),
[iquote('0:Rew:183.0,187.0')] ).
cnf(207,plain,
equal(store(a_35,i3,e_38),a_37),
inference(rew,[status(thm),theory(equality)],[205,11]),
[iquote('0:Rew:205.0,11.0')] ).
cnf(209,plain,
equal(select(a_37,i3),e_38),
inference(rew,[status(thm),theory(equality)],[205,101]),
[iquote('0:Rew:205.0,101.0')] ).
cnf(224,plain,
equal(e_38,e_36),
inference(rew,[status(thm),theory(equality)],[102,209]),
[iquote('0:Rew:102.0,209.0')] ).
cnf(226,plain,
equal(store(a_33,i3,e_36),a_33),
inference(rew,[status(thm),theory(equality)],[224,79]),
[iquote('0:Rew:224.0,79.0')] ).
cnf(230,plain,
equal(a_37,a_35),
inference(rew,[status(thm),theory(equality)],[80,207,224]),
[iquote('0:Rew:80.0,207.0,224.0,207.0')] ).
cnf(231,plain,
equal(store(a_33,i3,e_36),a_35),
inference(rew,[status(thm),theory(equality)],[230,10]),
[iquote('0:Rew:230.0,10.0')] ).
cnf(254,plain,
equal(a_35,a_33),
inference(rew,[status(thm),theory(equality)],[226,231]),
[iquote('0:Rew:226.0,231.0')] ).
cnf(256,plain,
equal(store(a_31,i2,e_34),a_33),
inference(rew,[status(thm),theory(equality)],[254,9]),
[iquote('0:Rew:254.0,9.0')] ).
cnf(258,plain,
equal(select(a_33,i2),e_34),
inference(rew,[status(thm),theory(equality)],[254,103]),
[iquote('0:Rew:254.0,103.0')] ).
cnf(277,plain,
equal(e_34,e_32),
inference(rew,[status(thm),theory(equality)],[104,258]),
[iquote('0:Rew:104.0,258.0')] ).
cnf(279,plain,
equal(store(a_29,i2,e_32),a_29),
inference(rew,[status(thm),theory(equality)],[277,81]),
[iquote('0:Rew:277.0,81.0')] ).
cnf(284,plain,
equal(a_33,a_31),
inference(rew,[status(thm),theory(equality)],[82,256,277]),
[iquote('0:Rew:82.0,256.0,277.0,256.0')] ).
cnf(285,plain,
equal(store(a_29,i2,e_32),a_31),
inference(rew,[status(thm),theory(equality)],[284,8]),
[iquote('0:Rew:284.0,8.0')] ).
cnf(313,plain,
equal(a_31,a_29),
inference(rew,[status(thm),theory(equality)],[279,285]),
[iquote('0:Rew:279.0,285.0')] ).
cnf(315,plain,
equal(store(a2,i1,e_30),a_29),
inference(rew,[status(thm),theory(equality)],[313,7]),
[iquote('0:Rew:313.0,7.0')] ).
cnf(317,plain,
equal(select(a_29,i1),e_30),
inference(rew,[status(thm),theory(equality)],[313,105]),
[iquote('0:Rew:313.0,105.0')] ).
cnf(340,plain,
equal(e_30,e_28),
inference(rew,[status(thm),theory(equality)],[106,317]),
[iquote('0:Rew:106.0,317.0')] ).
cnf(342,plain,
equal(store(a1,i1,e_28),a1),
inference(rew,[status(thm),theory(equality)],[340,83]),
[iquote('0:Rew:340.0,83.0')] ).
cnf(348,plain,
equal(a2,a_29),
inference(rew,[status(thm),theory(equality)],[84,315,340]),
[iquote('0:Rew:84.0,315.0,340.0,315.0')] ).
cnf(349,plain,
~ equal(a1,a_29),
inference(rew,[status(thm),theory(equality)],[348,35]),
[iquote('0:Rew:348.0,35.0')] ).
cnf(355,plain,
equal(a1,a_29),
inference(rew,[status(thm),theory(equality)],[6,342]),
[iquote('0:Rew:6.0,342.0')] ).
cnf(356,plain,
$false,
inference(mrr,[status(thm)],[355,349]),
[iquote('0:MRR:355.0,349.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV558-1.007 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.12 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n023.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 Jun 14 22:47:50 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.44
% 0.19/0.44 SPASS V 3.9
% 0.19/0.44 SPASS beiseite: Proof found.
% 0.19/0.44 % SZS status Theorem
% 0.19/0.44 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 SPASS derived 267 clauses, backtracked 0 clauses, performed 0 splits and kept 243 clauses.
% 0.19/0.44 SPASS allocated 63325 KBytes.
% 0.19/0.44 SPASS spent 0:00:00.08 on the problem.
% 0.19/0.44 0:00:00.04 for the input.
% 0.19/0.44 0:00:00.00 for the FLOTTER CNF translation.
% 0.19/0.44 0:00:00.00 for inferences.
% 0.19/0.44 0:00:00.00 for the backtracking.
% 0.19/0.44 0:00:00.02 for the reduction.
% 0.19/0.44
% 0.19/0.44
% 0.19/0.44 Here is a proof with depth 1, length 110 :
% 0.19/0.44 % SZS output start Refutation
% See solution above
% 0.19/0.44 Formulae used in the proof : a1 a3 hyp0 hyp1 hyp2 hyp3 hyp4 hyp5 hyp6 hyp7 hyp8 hyp9 hyp10 hyp11 hyp12 hyp13 hyp14 hyp15 hyp16 hyp17 hyp18 hyp19 hyp20 hyp21 hyp22 hyp23 hyp24 hyp25 hyp26 hyp27 hyp28 goal
% 0.19/0.44
%------------------------------------------------------------------------------