%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : COL003-15 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% 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 : Fri Jul 15 00:41:34 EDT 2022
% Result : Unsatisfiable 68.62s 68.86s
% Output : Refutation 68.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 4
% Syntax : Number of clauses : 29 ( 29 unt; 0 nHn; 3 RR)
% Number of literals : 29 ( 28 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 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 : 60 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(b_definition,axiom,
apply(apply(apply(b,X),Y),Z) = apply(X,apply(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_definition) ).
cnf(w_definition,axiom,
apply(apply(w,X),Y) = apply(apply(X,Y),Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',w_definition) ).
cnf(strong_fixed_point,axiom,
strong_fixed_point = apply(apply(b,apply(apply(b,apply(w,w)),w)),apply(apply(b,b),b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',strong_fixed_point) ).
cnf(prove_strong_fixed_point,negated_conjecture,
apply(strong_fixed_point,fixed_pt) != apply(fixed_pt,apply(strong_fixed_point,fixed_pt)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_strong_fixed_point) ).
cnf(5,plain,
apply(apply(w,w),X) = apply(apply(X,X),X),
inference('PARAMODULATE',[status(thm)],[w_definition,w_definition,theory(equality)]) ).
cnf(6,plain,
apply(apply(w,apply(w,X)),Y) = apply(apply(apply(X,Y),Y),Y),
inference('PARAMODULATE',[status(thm)],[w_definition,w_definition,theory(equality)]) ).
cnf(7,plain,
apply(apply(w,apply(X,Y)),Y) = apply(apply(apply(w,X),Y),Y),
inference('PARAMODULATE',[status(thm)],[w_definition,w_definition,theory(equality)]) ).
cnf(8,plain,
apply(apply(w,apply(b,X)),Y) = apply(X,apply(Y,Y)),
inference('PARAMODULATE',[status(thm)],[w_definition,b_definition,theory(equality)]) ).
cnf(10,plain,
apply(apply(apply(b,X),apply(w,Y)),Z) = apply(X,apply(apply(Y,Z),Z)),
inference('PARAMODULATE',[status(thm)],[b_definition,w_definition,theory(equality)]) ).
cnf(11,plain,
apply(apply(apply(b,X),apply(Y,Z)),Z) = apply(X,apply(apply(w,Y),Z)),
inference('PARAMODULATE',[status(thm)],[b_definition,w_definition,theory(equality)]) ).
cnf(13,plain,
apply(apply(apply(apply(b,w),X),Y),Z) = apply(apply(apply(X,Y),Z),Z),
inference('PARAMODULATE',[status(thm)],[w_definition,b_definition,theory(equality)]) ).
cnf(14,plain,
apply(apply(apply(b,X),apply(apply(b,Y),Z)),U) = apply(X,apply(Y,apply(Z,U))),
inference('PARAMODULATE',[status(thm)],[b_definition,b_definition,theory(equality)]) ).
cnf(15,plain,
apply(apply(apply(b,X),Y),apply(Z,U)) = apply(X,apply(apply(apply(b,Y),Z),U)),
inference('PARAMODULATE',[status(thm)],[b_definition,b_definition,theory(equality)]) ).
cnf(20,plain,
apply(strong_fixed_point,X) = apply(apply(apply(b,apply(w,w)),w),apply(apply(apply(b,b),b),X)),
inference('PARAMODULATE',[status(thm)],[b_definition,strong_fixed_point,theory(equality)]) ).
cnf(76,plain,
apply(apply(apply(X,Y),Y),Y) = apply(apply(apply(w,X),Y),Y),
inference('PARAMODULATE',[status(thm)],[w_definition,6,theory(equality)]) ).
cnf(100,plain,
apply(apply(apply(apply(b,w),X),Y),Y) = apply(apply(apply(w,X),Y),Y),
inference('PARAMODULATE',[status(thm)],[7,b_definition,theory(equality)]) ).
cnf(341,plain,
apply(apply(apply(b,X),apply(w,w)),Y) = apply(apply(apply(b,X),apply(Y,Y)),Y),
inference('PARAMODULATE',[status(thm)],[10,11,theory(equality)]) ).
cnf(620,plain,
apply(apply(apply(apply(b,w),apply(b,w)),X),Y) = apply(apply(apply(X,Y),Y),Y),
inference('PARAMODULATE',[status(thm)],[13,13,theory(equality)]) ).
cnf(646,plain,
apply(apply(apply(apply(b,w),X),apply(Y,Z)),U) = apply(apply(apply(apply(apply(b,X),Y),Z),U),U),
inference('PARAMODULATE',[status(thm)],[13,b_definition,theory(equality)]) ).
cnf(1256,plain,
apply(apply(apply(apply(b,w),apply(b,w)),X),Y) = apply(apply(apply(w,X),Y),Y),
inference('PARAMODULATE',[status(thm)],[13,100,theory(equality)]) ).
cnf(1497,plain,
apply(X,apply(Y,apply(Z,U))) = apply(X,apply(apply(apply(b,Y),Z),U)),
inference('PARAMODULATE',[status(thm)],[b_definition,14,theory(equality)]) ).
cnf(1498,plain,
apply(strong_fixed_point,X) = apply(apply(apply(b,apply(w,w)),w),apply(b,apply(b,X))),
inference('PARAMODULATE',[status(thm)],[14,strong_fixed_point,theory(equality)]) ).
cnf(1778,plain,
apply(apply(apply(apply(b,w),apply(b,w)),apply(X,apply(Y,Z))),U) = apply(apply(apply(apply(b,w),w),apply(X,apply(Y,Z))),U),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[76,1497,theory(equality)]),646,15,620,theory(equality)]) ).
cnf(1901,plain,
apply(strong_fixed_point,X) = apply(apply(w,w),apply(w,apply(b,apply(b,X)))),
inference('PARAMODULATE',[status(thm)],[b_definition,1498,theory(equality)]) ).
cnf(1918,plain,
apply(strong_fixed_point,X) = apply(apply(w,w),apply(apply(apply(b,w),b),apply(b,X))),
inference('PARAMODULATE',[status(thm)],[1497,1901,theory(equality)]) ).
cnf(2267,plain,
apply(apply(apply(b,X),apply(w,w)),apply(apply(apply(b,w),b),apply(b,Y))) = apply(X,apply(strong_fixed_point,Y)),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[15,20,theory(equality)]),15,theory(equality)]) ).
cnf(3389,plain,
apply(apply(apply(b,X),apply(w,w)),Y) = apply(apply(apply(apply(b,w),w),apply(b,apply(b,X))),Y),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[341,8,theory(equality)]),1778,1256,theory(equality)]) ).
cnf(8274,plain,
apply(strong_fixed_point,X) = apply(X,apply(strong_fixed_point,X)),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[5,1918,theory(equality)]),2267,3389,646,theory(equality)]) ).
cnf(8276,plain,
$false,
inference('REWRITE',[status(thm)],[prove_strong_fixed_point,8274,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : COL003-15 : TPTP v8.1.0. Released v2.1.0.
% 0.11/0.13 % Command : run-snark %s %d
% 0.13/0.33 % Computer : n023.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 : 600
% 0.13/0.33 % DateTime : Tue May 31 06:16:11 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.45 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 *
% 0.19/0.46 *
% 0.19/0.46 #<PACKAGE "SNARK-USER">
% 0.19/0.46 *
% 0.19/0.46 SNARK-TPTP-OPTIONS
% 0.19/0.46 *
% 0.19/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.46 (USE-FACTORING :POS)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.46 *
% 0.19/0.46 "."
% 0.19/0.46 *
% 0.19/0.47 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-05-31T06:16:12
% 0.19/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n023.cluster.edu at 2022-05-31T06:16:12
% 68.62/68.86
% 68.62/68.86
% 68.62/68.86 #||
% 68.62/68.86 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.62/68.86 % SZS output start Refutation
% See solution above
% 68.62/68.88 ||#
% 68.62/68.88
% 68.62/68.88 ; Summary of computation:
% 68.62/68.88 ; 26740 formulas have been input or derived (from 88 formulas).
% 68.62/68.88 ; 8276 (31%) were retained. Of these,
% 68.62/68.88 ; 1161 (14%) were simplified or subsumed later,
% 68.62/68.88 ; 7115 (86%) are still being kept.
% 68.62/68.88 ;
% 68.62/68.88 ; Run time in seconds excluding printing time:
% 68.62/68.88 ; 0.002 0% Read assertion file (1 call)
% 68.62/68.88 ; 0.000 0% Assert (4 calls)
% 68.62/68.88 ; 1.377 2% Process new row (26,597 calls)
% 68.62/68.88 ; 0.040 0% Resolution (174 calls)
% 68.62/68.88 ; 0.616 1% Paramodulation (87 calls)
% 68.62/68.88 ; 21.946 32% Forward simplification (26,502 calls)
% 68.62/68.88 ; 3.055 4% Backward simplification (8,276 calls)
% 68.62/68.88 ; 41.215 60% Ordering (4,604,960 calls)
% 68.62/68.88 ; 0.000 0% Sortal reasoning (32 calls)
% 68.62/68.88 ; 0.000 0% Purity testing (1 call)
% 68.62/68.88 ; 0.142 0% Other
% 68.62/68.88 ; 68.393 Total
% 68.62/68.88 ; 68.416 Real time
% 68.62/68.88 ;
% 68.62/68.88 ; Term-hash-array has 25,150 terms in all.
% 68.62/68.88 ; Feature-vector-row-index has 0 entries (0 at peak, 0 added, 0 deleted).
% 68.62/68.88 ; Feature-vector-row-index has 1 node (1 at peak, 1 added, 0 deleted).
% 68.62/68.88 ; Path-index has 22,473 entries (22,476 at peak, 25,718 added, 3,245 deleted).
% 68.62/68.88 ; Path-index has 2,084 nodes (2,090 at peak, 2,172 added, 88 deleted).
% 68.62/68.88 ; Trie-index has 22,473 entries (22,476 at peak, 25,718 added, 3,245 deleted).
% 68.62/68.88 ; Trie-index has 149,712 nodes (149,725 at peak, 171,176 added, 21,464 deleted).
% 68.62/68.88 ; Retrieved 10,245,819 generalization terms in 506,786 calls.
% 68.62/68.88 ; Retrieved 990,479 instance terms in 22,155 calls.
% 68.62/68.88 ; Retrieved 310,425 unifiable terms in 971 calls.
% 68.62/68.88 ;
% 68.62/68.88 ; The agenda of rows to process has 35 entries:
% 68.62/68.88 ; 1 with value 44 1 with value 50 2 with value 57
% 68.62/68.88 ; 3 with value 45 1 with value 51 1 with value 60
% 68.62/68.88 ; 2 with value 46 2 with value 52 2 with value 62
% 68.62/68.88 ; 3 with value 47 1 with value 53 5 with value 65
% 68.62/68.88 ; 1 with value 48 3 with value 54 1 with value 69
% 68.62/68.88 ; 3 with value 49 3 with value 56
% 68.62/68.88 ; The agenda of rows to give has 7030 entries:
% 68.62/68.88 ; 1 with value (4 17) 369 with value (4 44) 7 with value (4 62)
% 68.62/68.88 ; 41 with value (4 27) 237 with value (4 45) 6 with value (4 63)
% 68.62/68.88 ; 32 with value (4 28) 270 with value (4 46) 12 with value (4 64)
% 68.62/68.88 ; 71 with value (4 29) 193 with value (4 47) 7 with value (4 65)
% 68.62/68.88 ; 89 with value (4 30) 157 with value (4 48) 6 with value (4 66)
% 68.62/68.88 ; 111 with value (4 31) 116 with value (4 49) 3 with value (4 67)
% 68.62/68.88 ; 138 with value (4 32) 94 with value (4 50) 3 with value (4 68)
% 68.62/68.88 ; 226 with value (4 33) 69 with value (4 51) 1 with value (4 69)
% 68.62/68.88 ; 283 with value (4 34) 87 with value (4 52) 2 with value (4 70)
% 68.62/68.88 ; 270 with value (4 35) 53 with value (4 53) 3 with value (4 71)
% 68.62/68.88 ; 415 with value (4 36) 53 with value (4 54) 3 with value (4 72)
% 68.62/68.88 ; 397 with value (4 37) 41 with value (4 55) 1 with value (4 73)
% 68.62/68.88 ; 493 with value (4 38) 17 with value (4 56) 1 with value (4 74)
% 68.62/68.88 ; 657 with value (4 39) 12 with value (4 57) 1 with value (4 76)
% 68.62/68.88 ; 679 with value (4 40) 18 with value (4 58) 1 with value (4 77)
% 68.62/68.88 ; 491 with value (4 41) 22 with value (4 59) 1 with value (4 79)
% 68.62/68.88 ; 463 with value (4 42) 12 with value (4 60) 1 with value (4 81)
% 68.62/68.88 ; 282 with value (4 43) 11 with value (4 61) 1 with value (4 84)
% 68.62/68.88 Evaluation took:
% 68.62/68.88 68.418 seconds of real time
% 68.62/68.88 63.14987 seconds of user run time
% 68.62/68.88 5.265361 seconds of system run time
% 68.62/68.88 [Run times include 6.857 seconds GC run time.]
% 68.62/68.88 0 calls to %EVAL
% 68.62/68.88 0 page faults and
% 68.62/68.88 4,862,852,176 bytes consed.
% 68.62/68.88 :PROOF-FOUND
% 68.62/68.88 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-05-31T06:17:20
% 68.62/68.88 :PROOF-FOUND
% 68.62/68.88 *
%------------------------------------------------------------------------------