%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : GRA014+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n024.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 : 300s
% DateTime : Wed Jul 27 12:55:42 EDT 2022
% Result : Theorem 4.49s 4.70s
% Output : Refutation 4.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 10
% Syntax : Number of clauses : 129 ( 26 unt; 100 nHn; 129 RR)
% Number of literals : 302 ( 0 equ; 10 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 2 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 11 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ red(A,B)
| ~ red(B,C)
| ~ red(A,C)
| goal ),
file('GRA014+1.p',unknown),
[] ).
cnf(2,axiom,
( ~ green(A,B)
| ~ green(B,C)
| ~ green(A,C)
| goal ),
file('GRA014+1.p',unknown),
[] ).
cnf(3,axiom,
( ~ less_than(A,B)
| ~ less_than(B,C)
| less_than(A,C) ),
file('GRA014+1.p',unknown),
[] ).
cnf(4,axiom,
( ~ less_than(A,B)
| red(A,B)
| green(A,B) ),
file('GRA014+1.p',unknown),
[] ).
cnf(5,axiom,
~ goal,
file('GRA014+1.p',unknown),
[] ).
cnf(8,axiom,
less_than(n1,n2),
file('GRA014+1.p',unknown),
[] ).
cnf(9,axiom,
less_than(n2,n3),
file('GRA014+1.p',unknown),
[] ).
cnf(10,axiom,
less_than(n3,n4),
file('GRA014+1.p',unknown),
[] ).
cnf(11,axiom,
less_than(n4,n5),
file('GRA014+1.p',unknown),
[] ).
cnf(12,axiom,
less_than(n5,n6),
file('GRA014+1.p',unknown),
[] ).
cnf(13,plain,
( red(n1,n2)
| green(n1,n2) ),
inference(hyper,[status(thm)],[8,4]),
[iquote('hyper,8,4')] ).
cnf(14,plain,
( red(n2,n3)
| green(n2,n3) ),
inference(hyper,[status(thm)],[9,4]),
[iquote('hyper,9,4')] ).
cnf(15,plain,
less_than(n1,n3),
inference(hyper,[status(thm)],[9,3,8]),
[iquote('hyper,9,3,8')] ).
cnf(16,plain,
( red(n3,n4)
| green(n3,n4) ),
inference(hyper,[status(thm)],[10,4]),
[iquote('hyper,10,4')] ).
cnf(17,plain,
less_than(n2,n4),
inference(hyper,[status(thm)],[10,3,9]),
[iquote('hyper,10,3,9')] ).
cnf(18,plain,
( red(n4,n5)
| green(n4,n5) ),
inference(hyper,[status(thm)],[11,4]),
[iquote('hyper,11,4')] ).
cnf(19,plain,
less_than(n3,n5),
inference(hyper,[status(thm)],[11,3,10]),
[iquote('hyper,11,3,10')] ).
cnf(20,plain,
( red(n5,n6)
| green(n5,n6) ),
inference(hyper,[status(thm)],[12,4]),
[iquote('hyper,12,4')] ).
cnf(21,plain,
less_than(n4,n6),
inference(hyper,[status(thm)],[12,3,11]),
[iquote('hyper,12,3,11')] ).
cnf(22,plain,
( red(n1,n3)
| green(n1,n3) ),
inference(hyper,[status(thm)],[15,4]),
[iquote('hyper,15,4')] ).
cnf(23,plain,
less_than(n1,n4),
inference(hyper,[status(thm)],[15,3,10]),
[iquote('hyper,15,3,10')] ).
cnf(24,plain,
( red(n2,n4)
| green(n2,n4) ),
inference(hyper,[status(thm)],[17,4]),
[iquote('hyper,17,4')] ).
cnf(25,plain,
less_than(n2,n5),
inference(hyper,[status(thm)],[17,3,11]),
[iquote('hyper,17,3,11')] ).
cnf(26,plain,
( red(n3,n5)
| green(n3,n5) ),
inference(hyper,[status(thm)],[19,4]),
[iquote('hyper,19,4')] ).
cnf(27,plain,
less_than(n1,n5),
inference(hyper,[status(thm)],[19,3,15]),
[iquote('hyper,19,3,15')] ).
cnf(28,plain,
less_than(n3,n6),
inference(hyper,[status(thm)],[19,3,12]),
[iquote('hyper,19,3,12')] ).
cnf(29,plain,
( red(n4,n6)
| green(n4,n6) ),
inference(hyper,[status(thm)],[21,4]),
[iquote('hyper,21,4')] ).
cnf(30,plain,
less_than(n2,n6),
inference(hyper,[status(thm)],[21,3,17]),
[iquote('hyper,21,3,17')] ).
cnf(31,plain,
( red(n1,n4)
| green(n1,n4) ),
inference(hyper,[status(thm)],[23,4]),
[iquote('hyper,23,4')] ).
cnf(32,plain,
less_than(n1,n6),
inference(hyper,[status(thm)],[23,3,21]),
[iquote('hyper,23,3,21')] ).
cnf(33,plain,
( red(n2,n5)
| green(n2,n5) ),
inference(hyper,[status(thm)],[25,4]),
[iquote('hyper,25,4')] ).
cnf(34,plain,
( red(n1,n5)
| green(n1,n5) ),
inference(hyper,[status(thm)],[27,4]),
[iquote('hyper,27,4')] ).
cnf(35,plain,
( red(n3,n6)
| green(n3,n6) ),
inference(hyper,[status(thm)],[28,4]),
[iquote('hyper,28,4')] ).
cnf(36,plain,
( red(n2,n6)
| green(n2,n6) ),
inference(hyper,[status(thm)],[30,4]),
[iquote('hyper,30,4')] ).
cnf(37,plain,
( red(n1,n6)
| green(n1,n6) ),
inference(hyper,[status(thm)],[32,4]),
[iquote('hyper,32,4')] ).
cnf(38,plain,
( green(n1,n3)
| green(n1,n2)
| green(n2,n3) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[22,1,13,14]),5]),
[iquote('hyper,22,1,13,14,unit_del,5')] ).
cnf(39,plain,
( green(n2,n4)
| green(n2,n3)
| green(n3,n4) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[24,1,14,16]),5]),
[iquote('hyper,24,1,14,16,unit_del,5')] ).
cnf(40,plain,
( green(n3,n5)
| green(n3,n4)
| green(n4,n5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[26,1,16,18]),5]),
[iquote('hyper,26,1,16,18,unit_del,5')] ).
cnf(41,plain,
( green(n4,n6)
| green(n4,n5)
| green(n5,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[29,1,18,20]),5]),
[iquote('hyper,29,1,18,20,unit_del,5')] ).
cnf(42,plain,
( green(n1,n4)
| green(n1,n3)
| green(n3,n4) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[31,1,22,16]),5]),
[iquote('hyper,31,1,22,16,unit_del,5')] ).
cnf(43,plain,
( green(n1,n4)
| green(n1,n2)
| green(n2,n4) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[31,1,13,24]),5]),
[iquote('hyper,31,1,13,24,unit_del,5')] ).
cnf(44,plain,
( green(n2,n5)
| green(n2,n4)
| green(n4,n5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[33,1,24,18]),5]),
[iquote('hyper,33,1,24,18,unit_del,5')] ).
cnf(45,plain,
( green(n2,n5)
| green(n2,n3)
| green(n3,n5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[33,1,14,26]),5]),
[iquote('hyper,33,1,14,26,unit_del,5')] ).
cnf(46,plain,
( green(n1,n5)
| green(n1,n4)
| green(n4,n5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[34,1,31,18]),5]),
[iquote('hyper,34,1,31,18,unit_del,5')] ).
cnf(47,plain,
( green(n1,n5)
| green(n1,n3)
| green(n3,n5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[34,1,22,26]),5]),
[iquote('hyper,34,1,22,26,unit_del,5')] ).
cnf(48,plain,
( green(n1,n5)
| green(n1,n2)
| green(n2,n5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[34,1,13,33]),5]),
[iquote('hyper,34,1,13,33,unit_del,5')] ).
cnf(49,plain,
( green(n3,n6)
| green(n3,n5)
| green(n5,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[35,1,26,20]),5]),
[iquote('hyper,35,1,26,20,unit_del,5')] ).
cnf(50,plain,
( green(n3,n6)
| green(n3,n4)
| green(n4,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[35,1,16,29]),5]),
[iquote('hyper,35,1,16,29,unit_del,5')] ).
cnf(51,plain,
( green(n2,n6)
| green(n2,n5)
| green(n5,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[36,1,33,20]),5]),
[iquote('hyper,36,1,33,20,unit_del,5')] ).
cnf(52,plain,
( green(n2,n6)
| green(n2,n4)
| green(n4,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[36,1,24,29]),5]),
[iquote('hyper,36,1,24,29,unit_del,5')] ).
cnf(53,plain,
( green(n2,n6)
| green(n2,n3)
| green(n3,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[36,1,14,35]),5]),
[iquote('hyper,36,1,14,35,unit_del,5')] ).
cnf(54,plain,
( green(n1,n6)
| green(n1,n5)
| green(n5,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[37,1,34,20]),5]),
[iquote('hyper,37,1,34,20,unit_del,5')] ).
cnf(55,plain,
( green(n1,n6)
| green(n1,n4)
| green(n4,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[37,1,31,29]),5]),
[iquote('hyper,37,1,31,29,unit_del,5')] ).
cnf(56,plain,
( green(n1,n6)
| green(n1,n3)
| green(n3,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[37,1,22,35]),5]),
[iquote('hyper,37,1,22,35,unit_del,5')] ).
cnf(57,plain,
( green(n1,n6)
| green(n1,n2)
| green(n2,n6) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[37,1,13,36]),5]),
[iquote('hyper,37,1,13,36,unit_del,5')] ).
cnf(61,plain,
( green(n1,n4)
| green(n2,n4)
| green(n3,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[43,2,39,42]),5])])])]),
[iquote('hyper,43,2,39,42,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(63,plain,
( green(n2,n4)
| green(n4,n5)
| green(n3,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[44,2,39,40]),5])])])]),
[iquote('hyper,44,2,39,40,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(70,plain,
( green(n2,n5)
| green(n3,n5)
| green(n4,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[45,2,40,44]),5])])])]),
[iquote('hyper,45,2,40,44,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(75,plain,
( green(n1,n4)
| green(n4,n5)
| green(n2,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[46,2,43,44]),5])])])]),
[iquote('hyper,46,2,43,44,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(77,plain,
( green(n1,n4)
| green(n4,n5)
| green(n3,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[46,2,42,40]),5])])])]),
[iquote('hyper,46,2,42,40,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(90,plain,
( green(n1,n3)
| green(n3,n5)
| green(n3,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[47,2,42,40]),5])])])]),
[iquote('hyper,47,2,42,40,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(91,plain,
( green(n1,n3)
| green(n3,n5)
| green(n2,n3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[47,2,38,45]),5])])])]),
[iquote('hyper,47,2,38,45,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(93,plain,
( green(n1,n5)
| green(n3,n5)
| green(n4,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[47,2,40,46]),5])])])]),
[iquote('hyper,47,2,40,46,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(100,plain,
( green(n1,n2)
| green(n2,n5)
| green(n2,n3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[48,2,38,45]),5])])])]),
[iquote('hyper,48,2,38,45,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(101,plain,
( green(n1,n5)
| green(n2,n5)
| green(n3,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[48,2,45,47]),5])])])]),
[iquote('hyper,48,2,45,47,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(102,plain,
( green(n1,n5)
| green(n2,n5)
| green(n4,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[48,2,44,46]),5])])])]),
[iquote('hyper,48,2,44,46,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(103,plain,
( green(n1,n5)
| green(n1,n2)
| green(n1,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[48,2,43,46]),5])])])]),
[iquote('hyper,48,2,43,46,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(119,plain,
( green(n3,n4)
| green(n4,n6)
| green(n4,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[50,2,40,41]),5])])])]),
[iquote('hyper,50,2,40,41,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(128,plain,
( green(n3,n6)
| green(n4,n6)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[50,2,41,49]),5])])])]),
[iquote('hyper,50,2,41,49,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(131,plain,
( green(n3,n6)
| green(n3,n4)
| green(n3,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[50,2,40,49]),5])])])]),
[iquote('hyper,50,2,40,49,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(157,plain,
( green(n2,n4)
| green(n4,n6)
| green(n4,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[52,2,44,41]),5])])])]),
[iquote('hyper,52,2,44,41,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(158,plain,
( green(n2,n4)
| green(n4,n6)
| green(n3,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[52,2,39,50]),5])])])]),
[iquote('hyper,52,2,39,50,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(166,plain,
( green(n2,n6)
| green(n4,n6)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[52,2,41,51]),5])])])]),
[iquote('hyper,52,2,41,51,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(173,plain,
( green(n2,n3)
| green(n3,n6)
| green(n3,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[53,2,45,49]),5])])])]),
[iquote('hyper,53,2,45,49,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(178,plain,
( green(n2,n6)
| green(n3,n6)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[53,2,49,51]),5])])])]),
[iquote('hyper,53,2,49,51,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(184,plain,
( green(n2,n6)
| green(n2,n3)
| green(n2,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[53,2,45,51]),5])])])]),
[iquote('hyper,53,2,45,51,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(237,plain,
( green(n1,n4)
| green(n4,n6)
| green(n2,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[55,2,43,52]),5])])])]),
[iquote('hyper,55,2,43,52,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(250,plain,
( green(n1,n6)
| green(n4,n6)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[55,2,41,54]),5])])])]),
[iquote('hyper,55,2,41,54,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(271,plain,
( green(n1,n3)
| green(n3,n6)
| green(n3,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[56,2,42,50]),5])])])]),
[iquote('hyper,56,2,42,50,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(272,plain,
( green(n1,n3)
| green(n3,n6)
| green(n2,n3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[56,2,38,53]),5])])])]),
[iquote('hyper,56,2,38,53,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(275,plain,
( green(n1,n6)
| green(n3,n6)
| green(n4,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[56,2,50,55]),5])])])]),
[iquote('hyper,56,2,50,55,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(276,plain,
( green(n1,n6)
| green(n3,n6)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[56,2,49,54]),5])])])]),
[iquote('hyper,56,2,49,54,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(290,plain,
( green(n1,n2)
| green(n2,n6)
| green(n2,n3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[57,2,38,53]),5])])])]),
[iquote('hyper,57,2,38,53,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(291,plain,
( green(n1,n6)
| green(n2,n6)
| green(n3,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[57,2,53,56]),5])])])]),
[iquote('hyper,57,2,53,56,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(292,plain,
( green(n1,n6)
| green(n2,n6)
| green(n4,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[57,2,52,55]),5])])])]),
[iquote('hyper,57,2,52,55,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(293,plain,
( green(n1,n6)
| green(n2,n6)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[57,2,51,54]),5])])])]),
[iquote('hyper,57,2,51,54,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(297,plain,
( green(n1,n6)
| green(n1,n2)
| green(n1,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[57,2,43,55]),5])])])]),
[iquote('hyper,57,2,43,55,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(352,plain,
( green(n2,n4)
| green(n3,n4)
| green(n1,n6)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[63,2,61,54]),5])])]),
[iquote('hyper,63,2,61,54,unit_del,5,factor_simp,factor_simp')] ).
cnf(1009,plain,
( green(n3,n4)
| green(n1,n6)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[352,2,250,293]),5])])])])]),
[iquote('hyper,352,2,250,293,unit_del,5,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(1011,plain,
( green(n2,n4)
| green(n3,n4)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[352,2,61,158]),5])])])])]),
[iquote('hyper,352,2,61,158,unit_del,5,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(1014,plain,
( green(n1,n6)
| green(n5,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1009,2,250,276]),5])])])])]),
[iquote('hyper,1009,2,250,276,unit_del,5,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(1015,plain,
( green(n3,n4)
| green(n5,n6)
| green(n3,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1009,2,90,131]),5])])])]),
[iquote('hyper,1009,2,90,131,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(1016,plain,
( green(n3,n4)
| green(n5,n6)
| green(n4,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1009,2,77,119]),5])])])]),
[iquote('hyper,1009,2,77,119,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(1021,plain,
( green(n5,n6)
| green(n2,n5)
| green(n2,n3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1014,2,100,184]),5])])]),
[iquote('hyper,1014,2,100,184,unit_del,5,factor_simp,factor_simp')] ).
cnf(1023,plain,
( green(n5,n6)
| green(n3,n5)
| green(n2,n3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1014,2,91,173]),5])])]),
[iquote('hyper,1014,2,91,173,unit_del,5,factor_simp,factor_simp')] ).
cnf(1024,plain,
( green(n5,n6)
| green(n4,n5)
| green(n2,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1014,2,75,157]),5])])]),
[iquote('hyper,1014,2,75,157,unit_del,5,factor_simp,factor_simp')] ).
cnf(1037,plain,
( green(n2,n4)
| green(n3,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1011,2,63,158]),5])])])])]),
[iquote('hyper,1011,2,63,158,unit_del,5,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(1044,plain,
( green(n2,n4)
| green(n1,n6)
| green(n2,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1037,2,292,291]),5])])]),
[iquote('hyper,1037,2,292,291,unit_del,5,factor_simp,factor_simp')] ).
cnf(1045,plain,
( green(n2,n4)
| green(n1,n5)
| green(n2,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1037,2,102,101]),5])])]),
[iquote('hyper,1037,2,102,101,unit_del,5,factor_simp,factor_simp')] ).
cnf(1046,plain,
( green(n5,n6)
| green(n3,n5)
| green(n2,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1015,2,166,178]),5])])])]),
[iquote('hyper,1015,2,166,178,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(1179,plain,
( green(n5,n6)
| green(n3,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1046,2,1023,49]),5])])])])]),
[iquote('hyper,1046,2,1023,49,unit_del,5,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(1185,plain,
( green(n5,n6)
| green(n2,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1179,2,1037,1024]),5])])]),
[iquote('hyper,1179,2,1037,1024,unit_del,5,factor_simp,factor_simp')] ).
cnf(1190,plain,
( green(n2,n4)
| green(n1,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1185,2,75,237]),5])])])]),
[iquote('hyper,1185,2,75,237,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(1192,plain,
( green(n5,n6)
| green(n3,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1185,2,128,178]),5])])])]),
[iquote('hyper,1185,2,128,178,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(1209,plain,
( green(n2,n4)
| green(n2,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1190,2,52,1044]),5])])])]),
[iquote('hyper,1190,2,52,1044,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(1210,plain,
( green(n2,n4)
| green(n2,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1190,2,44,1045]),5])])])]),
[iquote('hyper,1190,2,44,1045,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(1216,plain,
( green(n5,n6)
| green(n4,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1192,2,1016,41]),5])])])]),
[iquote('hyper,1192,2,1016,41,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(1218,plain,
( green(n5,n6)
| green(n2,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1192,2,1021,51]),5])])])]),
[iquote('hyper,1192,2,1021,51,unit_del,5,factor_simp,factor_simp,factor_simp')] ).
cnf(1233,plain,
green(n2,n4),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1210,2,1185,1209]),5])])]),
[iquote('hyper,1210,2,1185,1209,unit_del,5,factor_simp,factor_simp')] ).
cnf(1240,plain,
( green(n1,n3)
| green(n3,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1233,2,272,271]),5])])]),
[iquote('hyper,1233,2,272,271,unit_del,5,factor_simp,factor_simp')] ).
cnf(1244,plain,
( green(n1,n3)
| green(n3,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1233,2,91,90]),5])])]),
[iquote('hyper,1233,2,91,90,unit_del,5,factor_simp,factor_simp')] ).
cnf(1246,plain,
( green(n1,n6)
| green(n3,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1233,2,275,291]),5])])]),
[iquote('hyper,1233,2,275,291,unit_del,5,factor_simp,factor_simp')] ).
cnf(1247,plain,
( green(n1,n5)
| green(n3,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1233,2,93,101]),5])])]),
[iquote('hyper,1233,2,93,101,unit_del,5,factor_simp,factor_simp')] ).
cnf(1254,plain,
green(n5,n6),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1218,2,1233,1216]),5])]),
[iquote('hyper,1218,2,1233,1216,unit_del,5,factor_simp')] ).
cnf(1257,plain,
( green(n1,n2)
| green(n1,n4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1254,2,103,297]),5])])]),
[iquote('hyper,1254,2,103,297,unit_del,5,factor_simp,factor_simp')] ).
cnf(1258,plain,
( green(n1,n2)
| green(n2,n3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1254,2,100,290]),5])])]),
[iquote('hyper,1254,2,100,290,unit_del,5,factor_simp,factor_simp')] ).
cnf(1279,plain,
green(n1,n3),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1244,2,1254,1240]),5])]),
[iquote('hyper,1244,2,1254,1240,unit_del,5,factor_simp')] ).
cnf(1290,plain,
( green(n2,n5)
| green(n4,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1279,2,70,102]),5])])]),
[iquote('hyper,1279,2,70,102,unit_del,5,factor_simp,factor_simp')] ).
cnf(1303,plain,
( green(n2,n3)
| green(n3,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1258,2,53,1246]),5])])]),
[iquote('hyper,1258,2,53,1246,unit_del,5,factor_simp,factor_simp')] ).
cnf(1304,plain,
( green(n2,n3)
| green(n3,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1258,2,45,1247]),5])])]),
[iquote('hyper,1258,2,45,1247,unit_del,5,factor_simp,factor_simp')] ).
cnf(1305,plain,
( green(n1,n2)
| green(n1,n5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1258,2,1247,48]),5])])]),
[iquote('hyper,1258,2,1247,48,unit_del,5,factor_simp,factor_simp')] ).
cnf(1306,plain,
( green(n1,n2)
| green(n1,n6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1258,2,1246,57]),5])])]),
[iquote('hyper,1258,2,1246,57,unit_del,5,factor_simp,factor_simp')] ).
cnf(1339,plain,
green(n2,n3),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1304,2,1254,1303]),5])]),
[iquote('hyper,1304,2,1254,1303,unit_del,5,factor_simp')] ).
cnf(1340,plain,
green(n1,n4),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1339,2,1257,1279]),5]),
[iquote('hyper,1339,2,1257,1279,unit_del,5')] ).
cnf(1345,plain,
green(n1,n5),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1305,2,1339,1279]),5]),
[iquote('hyper,1305,2,1339,1279,unit_del,5')] ).
cnf(1349,plain,
green(n2,n5),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1345,2,1340,1290]),5]),
[iquote('hyper,1345,2,1340,1290,unit_del,5')] ).
cnf(1354,plain,
green(n1,n6),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1306,2,1349,1345]),5]),
[iquote('hyper,1306,2,1349,1345,unit_del,5')] ).
cnf(1359,plain,
goal,
inference(hyper,[status(thm)],[1354,2,1345,1254]),
[iquote('hyper,1354,2,1345,1254')] ).
cnf(1360,plain,
$false,
inference(binary,[status(thm)],[1359,5]),
[iquote('binary,1359.1,5.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA014+1 : TPTP v8.1.0. Released v3.2.0.
% 0.00/0.12 % Command : otter-tptp-script %s
% 0.13/0.33 % Computer : n024.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Jul 27 02:23:25 EDT 2022
% 0.13/0.33 % CPUTime :
% 4.49/4.70 ----- Otter 3.3f, August 2004 -----
% 4.49/4.70 The process was started by sandbox2 on n024.cluster.edu,
% 4.49/4.70 Wed Jul 27 02:23:25 2022
% 4.49/4.70 The command was "./otter". The process ID is 17465.
% 4.49/4.70
% 4.49/4.70 set(prolog_style_variables).
% 4.49/4.70 set(auto).
% 4.49/4.70 dependent: set(auto1).
% 4.49/4.70 dependent: set(process_input).
% 4.49/4.70 dependent: clear(print_kept).
% 4.49/4.70 dependent: clear(print_new_demod).
% 4.49/4.70 dependent: clear(print_back_demod).
% 4.49/4.70 dependent: clear(print_back_sub).
% 4.49/4.70 dependent: set(control_memory).
% 4.49/4.70 dependent: assign(max_mem, 12000).
% 4.49/4.70 dependent: assign(pick_given_ratio, 4).
% 4.49/4.70 dependent: assign(stats_level, 1).
% 4.49/4.70 dependent: assign(max_seconds, 10800).
% 4.49/4.70 clear(print_given).
% 4.49/4.70
% 4.49/4.70 formula_list(usable).
% 4.49/4.70 all A B C (red(A,B)&red(B,C)&red(A,C)->goal).
% 4.49/4.70 all A B C (green(A,B)&green(B,C)&green(A,C)->goal).
% 4.49/4.70 less_than(n1,n2).
% 4.49/4.70 less_than(n2,n3).
% 4.49/4.70 less_than(n3,n4).
% 4.49/4.70 less_than(n4,n5).
% 4.49/4.70 less_than(n5,n6).
% 4.49/4.70 all A B C (less_than(A,B)&less_than(B,C)->less_than(A,C)).
% 4.49/4.70 all A B (less_than(A,B)->red(A,B)|green(A,B)).
% 4.49/4.70 -goal.
% 4.49/4.70 end_of_list.
% 4.49/4.70
% 4.49/4.70 -------> usable clausifies to:
% 4.49/4.70
% 4.49/4.70 list(usable).
% 4.49/4.70 0 [] -red(A,B)| -red(B,C)| -red(A,C)|goal.
% 4.49/4.70 0 [] -green(A,B)| -green(B,C)| -green(A,C)|goal.
% 4.49/4.70 0 [] less_than(n1,n2).
% 4.49/4.70 0 [] less_than(n2,n3).
% 4.49/4.70 0 [] less_than(n3,n4).
% 4.49/4.70 0 [] less_than(n4,n5).
% 4.49/4.70 0 [] less_than(n5,n6).
% 4.49/4.70 0 [] -less_than(A,B)| -less_than(B,C)|less_than(A,C).
% 4.49/4.70 0 [] -less_than(A,B)|red(A,B)|green(A,B).
% 4.49/4.70 0 [] -goal.
% 4.49/4.70 end_of_list.
% 4.49/4.70
% 4.49/4.70 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=4.
% 4.49/4.70
% 4.49/4.70 This is a non-Horn set without equality. The strategy will
% 4.49/4.70 be ordered hyper_res, unit deletion, and factoring, with
% 4.49/4.70 satellites in sos and with nuclei in usable.
% 4.49/4.70
% 4.49/4.70 dependent: set(hyper_res).
% 4.49/4.70 dependent: set(factor).
% 4.49/4.70 dependent: set(unit_deletion).
% 4.49/4.70
% 4.49/4.70 ------------> process usable:
% 4.49/4.70 ** KEPT (pick-wt=10): 1 [] -red(A,B)| -red(B,C)| -red(A,C)|goal.
% 4.49/4.70 ** KEPT (pick-wt=10): 2 [] -green(A,B)| -green(B,C)| -green(A,C)|goal.
% 4.49/4.70 ** KEPT (pick-wt=9): 3 [] -less_than(A,B)| -less_than(B,C)|less_than(A,C).
% 4.49/4.70 ** KEPT (pick-wt=9): 4 [] -less_than(A,B)|red(A,B)|green(A,B).
% 4.49/4.70 ** KEPT (pick-wt=1): 5 [] -goal.
% 4.49/4.70
% 4.49/4.70 ------------> process sos:
% 4.49/4.70 ** KEPT (pick-wt=3): 8 [] less_than(n1,n2).
% 4.49/4.70 ** KEPT (pick-wt=3): 9 [] less_than(n2,n3).
% 4.49/4.70 ** KEPT (pick-wt=3): 10 [] less_than(n3,n4).
% 4.49/4.70 ** KEPT (pick-wt=3): 11 [] less_than(n4,n5).
% 4.49/4.70 ** KEPT (pick-wt=3): 12 [] less_than(n5,n6).
% 4.49/4.70
% 4.49/4.70 ======= end of input processing =======
% 4.49/4.70
% 4.49/4.70 =========== start of search ===========
% 4.49/4.70
% 4.49/4.70 -------- PROOF --------
% 4.49/4.70
% 4.49/4.70 ----> UNIT CONFLICT at 2.80 sec ----> 1360 [binary,1359.1,5.1] $F.
% 4.49/4.70
% 4.49/4.70 Length of proof is 118. Level of proof is 22.
% 4.49/4.70
% 4.49/4.70 ---------------- PROOF ----------------
% 4.49/4.70 % SZS status Theorem
% 4.49/4.70 % SZS output start Refutation
% See solution above
% 4.49/4.70 ------------ end of proof -------------
% 4.49/4.70
% 4.49/4.70
% 4.49/4.70 Search stopped by max_proofs option.
% 4.49/4.70
% 4.49/4.70
% 4.49/4.70 Search stopped by max_proofs option.
% 4.49/4.70
% 4.49/4.70 ============ end of search ============
% 4.49/4.70
% 4.49/4.70 -------------- statistics -------------
% 4.49/4.70 clauses given 197
% 4.49/4.70 clauses generated 241231
% 4.49/4.70 clauses kept 1359
% 4.49/4.70 clauses forward subsumed 239881
% 4.49/4.70 clauses back subsumed 1316
% 4.49/4.70 Kbytes malloced 976
% 4.49/4.70
% 4.49/4.70 ----------- times (seconds) -----------
% 4.49/4.70 user CPU time 2.80 (0 hr, 0 min, 2 sec)
% 4.49/4.70 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 4.49/4.70 wall-clock time 4 (0 hr, 0 min, 4 sec)
% 4.49/4.70
% 4.49/4.70 That finishes the proof of the theorem.
% 4.49/4.70
% 4.49/4.70 Process 17465 finished Wed Jul 27 02:23:29 2022
% 4.49/4.70 Otter interrupted
% 4.49/4.70 PROOF FOUND
%------------------------------------------------------------------------------