%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ALG138+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% 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 : Thu Jul 14 17:59:59 EDT 2022
% Result : Unsatisfiable 0.19s 0.60s
% Output : Refutation 0.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 41
% Syntax : Number of clauses : 92 ( 59 unt; 29 nHn; 92 RR)
% Number of literals : 153 ( 152 equ; 52 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(13,axiom,
( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(14,axiom,
( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(15,axiom,
( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(21,axiom,
( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(25,axiom,
( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(29,axiom,
( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(33,axiom,
( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(35,axiom,
( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(44,axiom,
( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(49,axiom,
op(e0,e0) != op(e1,e0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(50,axiom,
op(e0,e0) != op(e2,e0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(51,axiom,
op(e0,e0) != op(e3,e0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(53,axiom,
op(e1,e0) != op(e3,e0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(54,axiom,
op(e2,e0) != op(e3,e0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(57,axiom,
op(e0,e1) != op(e3,e1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(58,axiom,
op(e1,e1) != op(e2,e1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(59,axiom,
op(e1,e1) != op(e3,e1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(60,axiom,
op(e2,e1) != op(e3,e1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(62,axiom,
op(e0,e2) != op(e2,e2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(63,axiom,
op(e0,e2) != op(e3,e2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(64,axiom,
op(e1,e2) != op(e2,e2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(65,axiom,
op(e1,e2) != op(e3,e2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(66,axiom,
op(e2,e2) != op(e3,e2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(67,axiom,
op(e0,e3) != op(e1,e3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(74,axiom,
op(e0,e0) != op(e0,e2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(83,axiom,
op(e1,e1) != op(e1,e3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(93,axiom,
op(e3,e0) != op(e3,e3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(95,axiom,
op(e3,e1) != op(e3,e3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(96,axiom,
op(e3,e2) != op(e3,e3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(97,axiom,
e0 != e1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(98,axiom,
e0 != e2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(100,axiom,
e1 != e2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(101,axiom,
e1 != e3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(103,axiom,
op(e0,e0) = e0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(104,axiom,
op(e1,e1) = e1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(105,axiom,
op(e2,e2) = e2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(106,axiom,
op(e3,e3) = e3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(107,axiom,
( op(e2,e3) != e0
| e1 != op(op(e2,e3),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(113,axiom,
( op(e2,e3) != e1
| e0 != op(op(e2,e3),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
cnf(127,axiom,
( op(e0,e2) != e3
| e1 != op(op(e0,e2),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
cnf(134,plain,
( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1 ),
inference('REWRITE',[status(thm)],[44,101,106,theory(equality)]) ).
cnf(143,plain,
op(e3,e0) != e3,
inference('REWRITE',[status(thm)],[93,106,theory(equality)]) ).
cnf(144,plain,
( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2 ),
inference('REWRITE',[status(thm)],[13,143]) ).
cnf(145,plain,
op(e3,e1) != e3,
inference('REWRITE',[status(thm)],[95,106,theory(equality)]) ).
cnf(146,plain,
( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2 ),
inference('REWRITE',[status(thm)],[14,145]) ).
cnf(147,plain,
op(e3,e2) != e3,
inference('REWRITE',[status(thm)],[96,106,theory(equality)]) ).
cnf(148,plain,
( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2 ),
inference('REWRITE',[status(thm)],[15,147]) ).
cnf(149,plain,
( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e3) = e0 ),
inference('REWRITE',[status(thm)],[33,98,105,theory(equality)]) ).
cnf(151,plain,
( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e3) = e1 ),
inference('REWRITE',[status(thm)],[35,100,105,theory(equality)]) ).
cnf(155,plain,
op(e0,e2) != e2,
inference('REWRITE',[status(thm)],[62,105,theory(equality)]) ).
cnf(156,plain,
( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e3 ),
inference('REWRITE',[status(thm)],[3,155]) ).
cnf(157,plain,
op(e1,e2) != e2,
inference('REWRITE',[status(thm)],[64,105,theory(equality)]) ).
cnf(159,plain,
op(e3,e2) != e2,
inference('REWRITE',[status(thm)],[66,105,theory(equality)]) ).
cnf(161,plain,
( op(e3,e2) = e0
| op(e3,e2) = e1 ),
inference('REWRITE',[status(thm)],[148,159]) ).
cnf(169,plain,
( op(e1,e0) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 ),
inference('REWRITE',[status(thm)],[25,97,104,theory(equality)]) ).
cnf(171,plain,
( op(e1,e0) = e2
| op(e1,e3) = e2 ),
inference('REWRITE',[status(thm)],[29,157,100,104,theory(equality)]) ).
cnf(177,plain,
op(e2,e1) != e1,
inference('REWRITE',[status(thm)],[58,104,theory(equality)]) ).
cnf(178,plain,
( op(e2,e0) = e1
| op(e2,e3) = e1 ),
inference('REWRITE',[status(thm)],[151,177]) ).
cnf(180,plain,
op(e3,e1) != e1,
inference('REWRITE',[status(thm)],[59,104,theory(equality)]) ).
cnf(182,plain,
( op(e3,e1) = e0
| op(e3,e1) = e2 ),
inference('REWRITE',[status(thm)],[146,180]) ).
cnf(188,plain,
op(e1,e3) != e1,
inference('REWRITE',[status(thm)],[83,104,theory(equality)]) ).
cnf(189,plain,
( op(e0,e3) = e1
| op(e2,e3) = e1 ),
inference('REWRITE',[status(thm)],[134,188]) ).
cnf(193,plain,
( op(e0,e1) = e2
| op(e0,e3) = e2 ),
inference('REWRITE',[status(thm)],[21,155,98,103,theory(equality)]) ).
cnf(197,plain,
op(e1,e0) != e0,
inference('REWRITE',[status(thm)],[49,103,theory(equality)]) ).
cnf(198,plain,
( op(e1,e2) = e0
| op(e1,e3) = e0 ),
inference('REWRITE',[status(thm)],[169,197]) ).
cnf(200,plain,
op(e2,e0) != e0,
inference('REWRITE',[status(thm)],[50,103,theory(equality)]) ).
cnf(201,plain,
( op(e2,e1) = e0
| op(e2,e3) = e0 ),
inference('REWRITE',[status(thm)],[149,200]) ).
cnf(203,plain,
op(e3,e0) != e0,
inference('REWRITE',[status(thm)],[51,103,theory(equality)]) ).
cnf(205,plain,
( op(e3,e0) = e1
| op(e3,e0) = e2 ),
inference('REWRITE',[status(thm)],[144,203]) ).
cnf(209,plain,
op(e0,e2) != e0,
inference('REWRITE',[status(thm)],[74,103,theory(equality)]) ).
cnf(211,plain,
( op(e0,e2) = e1
| op(e0,e2) = e3 ),
inference('REWRITE',[status(thm)],[156,209]) ).
cnf(253,plain,
( op(e2,e1) = e0
| op(e0,e3) = e1 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[189,201,theory(equality)]),97]) ).
cnf(278,plain,
( op(e2,e1) = e0
| op(e0,e3) != e1 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[107,201,theory(equality)]),theory(equality)]) ).
cnf(375,plain,
op(e2,e1) = e0,
inference('HYPERRESOLVE',[status(thm)],[278,253]) ).
cnf(376,plain,
op(e3,e1) != e0,
inference('REWRITE',[status(thm)],[60,375,theory(equality)]) ).
cnf(377,plain,
op(e3,e1) = e2,
inference('REWRITE',[status(thm)],[182,376]) ).
cnf(378,plain,
op(e0,e1) != e2,
inference('REWRITE',[status(thm)],[57,377,theory(equality)]) ).
cnf(379,plain,
op(e0,e3) = e2,
inference('REWRITE',[status(thm)],[193,378]) ).
cnf(380,plain,
op(e1,e3) != e2,
inference('REWRITE',[status(thm)],[67,379,theory(equality)]) ).
cnf(381,plain,
op(e1,e0) = e2,
inference('REWRITE',[status(thm)],[171,380]) ).
cnf(382,plain,
op(e3,e0) != e2,
inference('REWRITE',[status(thm)],[53,381,theory(equality)]) ).
cnf(383,plain,
op(e3,e0) = e1,
inference('REWRITE',[status(thm)],[205,382]) ).
cnf(384,plain,
op(e2,e0) != e1,
inference('REWRITE',[status(thm)],[54,383,theory(equality)]) ).
cnf(385,plain,
op(e2,e3) = e1,
inference('REWRITE',[status(thm)],[178,384]) ).
cnf(386,plain,
op(e1,e3) != e0,
inference('REWRITE',[status(thm)],[113,385,theory(equality)]) ).
cnf(387,plain,
op(e1,e2) = e0,
inference('REWRITE',[status(thm)],[198,386]) ).
cnf(388,plain,
op(e3,e2) != e0,
inference('REWRITE',[status(thm)],[65,387,theory(equality)]) ).
cnf(389,plain,
op(e3,e2) = e1,
inference('REWRITE',[status(thm)],[161,388]) ).
cnf(390,plain,
op(e0,e2) != e1,
inference('REWRITE',[status(thm)],[63,389,theory(equality)]) ).
cnf(391,plain,
op(e0,e2) = e3,
inference('REWRITE',[status(thm)],[211,390]) ).
cnf(394,plain,
$false,
inference('REWRITE',[status(thm)],[127,389,391,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ALG138+1 : TPTP v8.1.0. Released v2.7.0.
% 0.06/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Wed Jun 8 11:21:20 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.44 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 *
% 0.19/0.45 *
% 0.19/0.45 #<PACKAGE "SNARK-USER">
% 0.19/0.45 *
% 0.19/0.45 SNARK-TPTP-OPTIONS
% 0.19/0.45 *
% 0.19/0.45 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.45 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.45 (USE-FACTORING :POS)
% 0.19/0.45 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.45 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.45 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.45 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.45 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.45 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.45 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.45 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.45 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.45 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.45 *
% 0.19/0.45 "."
% 0.19/0.45 *
% 0.19/0.45 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-08T11:21:20
% 0.19/0.45 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n022.cluster.edu at 2022-06-08T11:21:20
% 0.19/0.60
% 0.19/0.60
% 0.19/0.60 #||
% 0.19/0.60 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.60 % SZS output start Refutation
% See solution above
% 0.44/0.61 ||#
% 0.44/0.61
% 0.44/0.61 ; Summary of computation:
% 0.44/0.61 ; 1274 formulas have been input or derived (from 183 formulas).
% 0.44/0.61 ; 394 (31%) were retained. Of these,
% 0.44/0.61 ; 362 (92%) were simplified or subsumed later,
% 0.44/0.61 ; 32 ( 8%) are still being kept.
% 0.44/0.61 ;
% 0.44/0.61 ; Run time in seconds excluding printing time:
% 0.44/0.61 ; 0.016 11% Read assertion file (1 call)
% 0.44/0.61 ; 0.011 8% Assert (29 calls)
% 0.44/0.61 ; 0.020 14% Process new row (1,055 calls)
% 0.44/0.61 ; 0.006 4% Resolution (364 calls)
% 0.44/0.61 ; 0.007 5% Paramodulation (182 calls)
% 0.44/0.61 ; 0.001 1% Factoring (50 calls)
% 0.44/0.61 ; 0.001 1% Condensing (486 calls)
% 0.44/0.61 ; 0.017 12% Forward subsumption (486 calls)
% 0.44/0.61 ; 0.009 6% Backward subsumption (292 calls)
% 0.44/0.61 ; 0.002 1% Clause clause subsumption (707 calls)
% 0.44/0.61 ; 0.015 10% Forward simplification (1,055 calls)
% 0.44/0.61 ; 0.015 10% Backward simplification (394 calls)
% 0.44/0.61 ; 0.004 3% Ordering (2,317 calls)
% 0.44/0.61 ; 0.000 0% Sortal reasoning (32 calls)
% 0.44/0.61 ; 0.000 0% Purity testing (1 call)
% 0.44/0.61 ; 0.021 14% Other
% 0.44/0.61 ; 0.145 Total
% 0.44/0.61 ; 0.157 Real time
% 0.44/0.61 ;
% 0.44/0.61 ; Term-hash-array has 170 terms in all.
% 0.44/0.61 ; Feature-vector-row-index has 0 entries (220 at peak, 292 added, 292 deleted).
% 0.44/0.61 ; Feature-vector-row-index has 1 node (805 at peak, 1,113 added, 1,112 deleted).
% 0.44/0.61 ; Retrieved 713 possibly forward subsuming rows in 486 calls.
% 0.44/0.61 ; Retrieved 214 possibly backward subsumed rows in 292 calls.
% 0.44/0.61 ; Path-index has 51 entries (138 at peak, 174 added, 123 deleted).
% 0.44/0.61 ; Path-index has 38 nodes (54 at peak, 54 added, 16 deleted).
% 0.44/0.61 ; Trie-index has 51 entries (138 at peak, 174 added, 123 deleted).
% 0.44/0.61 ; Trie-index has 82 nodes (261 at peak, 318 added, 236 deleted).
% 0.44/0.61 ; Retrieved 521 generalization terms in 3,755 calls.
% 0.44/0.61 ; Retrieved 101 instance terms in 101 calls.
% 0.44/0.61 ; Retrieved 548 unifiable terms in 1,302 calls.
% 0.44/0.61 ;
% 0.44/0.61 ; The agenda of backward simplifiable rows to process has 213 entries:
% 0.44/0.61 ; 213 with value 0
% 0.44/0.61 ; The agenda of rows to process has 6 entries:
% 0.44/0.61 ; 1 with value 13 1 with value 16 4 with value 20
% 0.44/0.61 ; The agenda of input rows to give has 13 entries:
% 0.44/0.61 ; 13 with value 7
% 0.44/0.61 ; The agenda of rows to give has 2 entries:
% 0.44/0.61 ; 1 with value (4 8) 1 with value (4 9)
% 0.44/0.61 Evaluation took:
% 0.44/0.61 0.157 seconds of real time
% 0.44/0.61 0.145567 seconds of user run time
% 0.44/0.61 0.010891 seconds of system run time
% 0.44/0.61 [Run times include 0.005 seconds GC run time.]
% 0.44/0.61 0 calls to %EVAL
% 0.44/0.61 0 page faults and
% 0.44/0.61 15,602,344 bytes consed.
% 0.44/0.61 :PROOF-FOUND
% 0.44/0.61 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-08T11:21:20
% 0.44/0.61 :PROOF-FOUND
% 0.44/0.61 *
%------------------------------------------------------------------------------