↑ Up

ZenonModulo---0.5.0.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : SYN435+1 : TPTP v8.2.0. Released v2.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n005.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 : Tue Jun 25 02:18:38 EDT 2024

% Result   : Unknown 0.59s 0.76s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SYN435+1 : TPTP v8.2.0. Released v2.1.0.
% 0.07/0.12  % Command  : run_zenon_modulo %d %s
% 0.12/0.33  % Computer : n005.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 300
% 0.12/0.33  % DateTime : Mon Jun 24 01:05:39 EDT 2024
% 0.12/0.33  % CPUTime  : 
% 0.59/0.76  Zenon error: exhausted search space without finding a proof
% 0.59/0.76  (* Current branch:
% 0.59/0.76  ((a303) != (a336))
% 0.59/0.76  ((a293) != (a290))
% 0.59/0.76  ((a330) != (a293))
% 0.59/0.76  ((a313) != (a312))
% 0.59/0.76  ((a285) != (a286))
% 0.59/0.76  (zenon_X22 != (a324))
% 0.59/0.76  ((a289) != (a312))
% 0.59/0.76  ((a302) != (a340))
% 0.59/0.76  ((a302) != (a312))
% 0.59/0.76  ((a334) != (a326))
% 0.59/0.76  ((a309) != (a327))
% 0.59/0.76  ((a340) != (a327))
% 0.59/0.76  ((a342) != (a324))
% 0.59/0.76  (-. (c2_1 (a317)))
% 0.59/0.76  ((a336) != (a347))
% 0.59/0.76  ((a288) != (a294))
% 0.59/0.76  ((a298) != (a347))
% 0.59/0.76  ((a302) != (a334))
% 0.59/0.76  ((a340) != (a342))
% 0.59/0.76  ((a331) != (a300))
% 0.59/0.76  ((a282) != (a327))
% 0.59/0.76  ((a289) != (a310))
% 0.59/0.76  ((a309) != (a305))
% 0.59/0.76  ((a335) != (a306))
% 0.59/0.76  ((a336) != zenon_X22)
% 0.59/0.76  ((a319) != (a310))
% 0.59/0.76  (-. (c3_1 (a330)))
% 0.59/0.76  ((a311) != (a299))
% 0.59/0.76  (c3_1 (a291))
% 0.59/0.76  ((a315) != (a304))
% 0.59/0.76  (c1_1 (a301))
% 0.59/0.76  ((a331) != (a337))
% 0.59/0.76  ((a331) != (a312))
% 0.59/0.76  (hskp30)
% 0.59/0.76  ((a300) != (a301))
% 0.59/0.76  ((a302) != (a311))
% 0.59/0.76  (zenon_X0 != (a318))
% 0.59/0.76  ((a291) != (a337))
% 0.59/0.76  ((a286) != (a336))
% 0.59/0.76  ((a334) != (a322))
% 0.59/0.76  ((a340) != (a335))
% 0.59/0.76  ((a289) != (a299))
% 0.59/0.76  (c0_1 (a287))
% 0.59/0.76  ((a303) != (a324))
% 0.59/0.76  ((a315) != (a301))
% 0.59/0.76  ((a335) != (a288))
% 0.59/0.76  ((a282) != (a333))
% 0.59/0.76  ((a288) != (a312))
% 0.59/0.76  (-. (c3_1 (a324)))
% 0.59/0.76  ((a307) != (a288))
% 0.59/0.76  ((a315) != (a300))
% 0.59/0.76  ((a325) != (a286))
% 0.59/0.76  ((a284) != (a286))
% 0.59/0.76  ((a302) != (a305))
% 0.59/0.76  ((a297) != (a305))
% 0.59/0.76  ((a303) != (a286))
% 0.59/0.76  ((a299) != (a309))
% 0.59/0.76  ((a325) != (a344))
% 0.59/0.76  (-. (c2_1 (a310)))
% 0.59/0.76  ((a293) != (a312))
% 0.59/0.76  ((a315) != (a347))
% 0.59/0.76  ((a334) != (a293))
% 0.59/0.76  ((a340) != (a311))
% 0.59/0.76  ((a344) != (a298))
% 0.59/0.76  ((a307) != (a305))
% 0.59/0.76  ((a307) != (a324))
% 0.59/0.76  ((a343) != (a334))
% 0.59/0.76  ((a285) != (a326))
% 0.59/0.76  ((a305) != (a324))
% 0.59/0.76  ((a326) != (a306))
% 0.59/0.76  (-. (c2_1 (a337)))
% 0.59/0.76  (-. (c1_1 (a316)))
% 0.59/0.76  ((a285) != (a309))
% 0.59/0.76  ((a307) != (a326))
% 0.59/0.76  ((a325) != (a306))
% 0.59/0.76  (zenon_X20 != (a283))
% 0.59/0.76  ((a305) != (a292))
% 0.59/0.76  ((a326) != (a310))
% 0.59/0.76  ((a315) != (a337))
% 0.59/0.76  ((a316) != (a327))
% 0.59/0.76  ((a309) != (a301))
% 0.59/0.76  ((a322) != (a324))
% 0.59/0.76  ((a325) != (a311))
% 0.59/0.76  ((a335) != (a347))
% 0.59/0.76  ((a325) != zenon_X22)
% 0.59/0.76  ((a296) != (a313))
% 0.59/0.76  ((a311) != (a306))
% 0.59/0.76  ((a313) != (a322))
% 0.59/0.76  ((a283) != (a309))
% 0.59/0.76  ((a309) != (a324))
% 0.59/0.76  (-. (c3_1 (a294)))
% 0.59/0.76  (c1_1 (a315))
% 0.59/0.76  ((a302) != (a342))
% 0.59/0.76  ((a286) != (a333))
% 0.59/0.76  ((a327) != (a283))
% 0.59/0.76  ((a289) != (a300))
% 0.59/0.76  ((a283) != (a293))
% 0.59/0.76  ((a287) != (a298))
% 0.59/0.76  ((a289) != (a347))
% 0.59/0.76  ((a325) != (a322))
% 0.59/0.76  ((a322) != (a306))
% 0.59/0.76  ((a336) != (a312))
% 0.59/0.76  ((a344) != (a312))
% 0.59/0.76  ((a287) != (a293))
% 0.59/0.76  ((a307) != (a292))
% 0.59/0.76  ((a335) != (a300))
% 0.59/0.76  (zenon_X0 != (a327))
% 0.59/0.76  ((a303) != (a326))
% 0.59/0.76  ((a286) != (a337))
% 0.59/0.76  ((a284) != (a344))
% 0.59/0.76  (hskp40)
% 0.59/0.76  ((a285) != (a290))
% 0.59/0.76  ((a317) != (a294))
% 0.59/0.76  ((a316) != (a319))
% 0.59/0.76  ((a305) != (a298))
% 0.59/0.76  ((a283) != (a333))
% 0.59/0.76  ((a287) != (a309))
% 0.59/0.76  (c0_1 (a282))
% 0.59/0.76  ((a303) != (a345))
% 0.59/0.76  ((a293) != (a286))
% 0.59/0.76  ((a285) != (a342))
% 0.59/0.76  (c1_1 (a302))
% 0.59/0.76  ((a343) != (a316))
% 0.59/0.76  ((a297) != (a292))
% 0.59/0.76  ((a289) != (a293))
% 0.59/0.76  ((a335) != (a344))
% 0.59/0.76  ((a297) != (a337))
% 0.59/0.76  ((a285) != (a284))
% 0.59/0.76  ((a289) != (a324))
% 0.59/0.76  ((a336) != (a324))
% 0.59/0.76  ((a296) != (a306))
% 0.59/0.76  (c0_1 (a297))
% 0.59/0.76  ((a343) != zenon_X22)
% 0.59/0.76  ((a336) != (a318))
% 0.59/0.76  ((a293) != (a301))
% 0.59/0.76  (-. (c2_1 (a306)))
% 0.59/0.76  ((a297) != (a301))
% 0.59/0.76  ((a282) != (a313))
% 0.59/0.76  ((a342) != (a298))
% 0.59/0.76  ((a300) != (a317))
% 0.59/0.76  ((a343) != (a344))
% 0.59/0.76  (c3_1 (a336))
% 0.59/0.76  ((a296) != (a312))
% 0.59/0.76  ((a303) != (a300))
% 0.59/0.76  ((a311) != (a294))
% 0.59/0.76  ((a315) != (a312))
% 0.59/0.76  ((a309) != (a342))
% 0.59/0.76  (hskp12)
% 0.59/0.76  ((a342) != (a330))
% 0.59/0.76  ((a326) != (a347))
% 0.59/0.76  ((a309) != (a307))
% 0.59/0.76  ((a307) != (a313))
% 0.59/0.76  (zenon_X0 != (a317))
% 0.59/0.76  (zenon_X20 != (a292))
% 0.59/0.76  ((a309) != (a306))
% 0.59/0.76  ((a301) != (a347))
% 0.59/0.76  ((a285) != (a334))
% 0.59/0.76  ((a331) != (a310))
% 0.59/0.76  (c1_1 (a285))
% 0.59/0.76  (-. (c2_1 (a291)))
% 0.59/0.76  ((a334) != (a306))
% 0.59/0.76  ((a342) != (a318))
% 0.59/0.76  (zenon_X10 != (a347))
% 0.59/0.76  ((a299) != (a310))
% 0.59/0.76  ((a303) != (a294))
% 0.59/0.76  ((a305) != (a318))
% 0.59/0.76  ((a298) != (a319))
% 0.59/0.76  ((a330) != (a318))
% 0.59/0.76  ((a331) != (a318))
% 0.59/0.76  (-. (c2_1 (a333)))
% 0.59/0.76  ((a291) != (a306))
% 0.59/0.76  ((a294) != (a309))
% 0.59/0.76  ((a343) != (a322))
% 0.59/0.76  ((a311) != (a312))
% 0.59/0.76  ((a325) != (a299))
% 0.59/0.76  ((a335) != (a305))
% 0.59/0.76  (zenon_X20 != (a324))
% 0.59/0.76  (zenon_X10 != (a325))
% 0.59/0.76  ((a299) != (a334))
% 0.59/0.76  ((a343) != (a335))
% 0.59/0.76  ((a300) != (a310))
% 0.59/0.76  (c1_1 (a331))
% 0.59/0.76  ((a287) != (a313))
% 0.59/0.76  ((a307) != (a300))
% 0.59/0.76  (zenon_X20 != (a298))
% 0.59/0.76  ((a282) != (a316))
% 0.59/0.76  ((a309) != (a316))
% 0.59/0.76  ((a345) != (a313))
% 0.59/0.76  ((a282) != (a290))
% 0.59/0.76  ((a316) != (a337))
% 0.59/0.76  ((a302) != (a283))
% 0.59/0.76  (zenon_X10 != (a306))
% 0.59/0.76  ((a326) != (a290))
% 0.59/0.76  ((a285) != (a293))
% 0.59/0.76  ((a331) != (a347))
% 0.59/0.76  ((a326) != (a318))
% 0.59/0.76  ((a315) != (a299))
% 0.59/0.76  ((a296) != (a316))
% 0.59/0.76  ((a345) != (a283))
% 0.59/0.76  (c0_1 (a302))
% 0.59/0.76  ((a296) != (a297))
% 0.59/0.76  (-. (c1_1 (a297)))
% 0.59/0.76  ((a285) != (a327))
% 0.59/0.76  (-. (c0_1 (a347)))
% 0.59/0.76  (zenon_X20 != (a335))
% 0.59/0.76  ((a316) != (a317))
% 0.59/0.76  ((a340) != (a283))
% 0.59/0.76  ((a297) != (a291))
% 0.59/0.76  (zenon_X20 != (a327))
% 0.59/0.76  (-. (c0_1 (a307)))
% 0.59/0.76  ((a302) != (a317))
% 0.59/0.76  ((a304) != (a301))
% 0.59/0.76  ((a305) != (a301))
% 0.59/0.76  ((a282) != (a310))
% 0.59/0.76  ((a315) != (a282))
% 0.59/0.76  ((a316) != (a318))
% 0.59/0.76  ((a311) != (a292))
% 0.59/0.76  (c0_1 (a311))
% 0.59/0.76  (zenon_X20 != (a312))
% 0.59/0.76  (zenon_X20 != (a330))
% 0.59/0.76  ((a344) != (a306))
% 0.59/0.76  ((a302) != (a344))
% 0.59/0.76  (c2_1 (a330))
% 0.59/0.76  (zenon_X0 != (a310))
% 0.59/0.76  ((a330) != (a317))
% 0.59/0.76  ((a343) != (a305))
% 0.59/0.76  ((a344) != (a318))
% 0.59/0.76  ((a344) != (a327))
% 0.59/0.76  ((a294) != (a291))
% 0.59/0.76  ((a287) != (a340))
% 0.59/0.76  (c0_1 (a330))
% 0.59/0.76  (-. (c0_1 (a334)))
% 0.59/0.76  ((a317) != (a318))
% 0.59/0.76  ((a334) != (a300))
% 0.59/0.76  ((a297) != (a336))
% 0.59/0.76  ((a303) != (a288))
% 0.59/0.76  ((a335) != (a294))
% 0.59/0.76  ((a343) != (a292))
% 0.59/0.76  ((a283) != (a347))
% 0.59/0.76  ((a307) != (a325))
% 0.59/0.76  ((a330) != (a292))
% 0.59/0.76  ((a284) != (a288))
% 0.59/0.76  ((a340) != (a293))
% 0.59/0.76  ((a313) != (a318))
% 0.59/0.76  ((a344) != (a292))
% 0.59/0.76  ((a298) != (a300))
% 0.59/0.76  ((a327) != (a324))
% 0.59/0.76  ((a315) != (a325))
% 0.59/0.76  ((a344) != (a333))
% 0.59/0.76  ((a305) != (a317))
% 0.59/0.76  ((a286) != (a318))
% 0.59/0.76  ((a344) != (a296))
% 0.59/0.76  ((a289) != (a309))
% 0.59/0.76  ((a304) != (a306))
% 0.59/0.76  ((a342) != (a284))
% 0.59/0.76  (hskp35)
% 0.59/0.76  ((a294) != (a337))
% 0.59/0.76  ((a335) != (a291))
% 0.59/0.76  ((a287) != (a286))
% 0.59/0.76  ((a343) != (a342))
% 0.59/0.76  (c3_1 (a313))
% 0.59/0.76  ((a297) != (a334))
% 0.59/0.76  ((a309) != (a310))
% 0.59/0.76  (c0_1 (a336))
% 0.59/0.76  ((a313) != (a300))
% 0.59/0.76  ((a317) != (a326))
% 0.59/0.76  ((a340) != (a290))
% 0.59/0.76  ((a315) != (a344))
% 0.59/0.76  ((a283) != (a318))
% 0.59/0.76  ((a303) != (a298))
% 0.59/0.76  ((a296) != (a305))
% 0.59/0.76  ((a303) != (a307))
% 0.59/0.76  ((a302) != (a331))
% 0.59/0.76  ((a343) != (a347))
% 0.59/0.76  ((a317) != (a282))
% 0.59/0.76  ((a303) != (a306))
% 0.59/0.76  ((a296) != (a319))
% 0.59/0.76  ((a291) != (a327))
% 0.59/0.76  ((a330) != (a309))
% 0.59/0.76  ((a340) != (a333))
% 0.59/0.76  (c0_1 (a303))
% 0.59/0.76  ((a322) != (a318))
% 0.59/0.76  ((a327) != (a292))
% 0.59/0.76  ((a287) != (a318))
% 0.59/0.76  ((a336) != (a306))
% 0.59/0.76  (-. (c3_1 (a310)))
% 0.59/0.76  ((a331) != (a335))
% 0.59/0.76  ((a301) != (a322))
% 0.59/0.76  ((a325) != (a342))
% 0.59/0.76  ((a345) != (a288))
% 0.59/0.76  (zenon_X20 != (a347))
% 0.59/0.76  ((a289) != (a313))
% 0.59/0.76  ((a285) != (a304))
% 0.59/0.76  ((a340) != (a325))
% 0.59/0.76  ((a342) != (a299))
% 0.59/0.76  ((a299) != (a290))
% 0.59/0.76  ((a296) != (a290))
% 0.59/0.76  ((a325) != (a312))
% 0.59/0.76  ((a331) != (a316))
% 0.59/0.76  ((a342) != (a310))
% 0.59/0.76  ((a294) != (a347))
% 0.59/0.76  ((a307) != (a322))
% 0.59/0.76  ((a325) != (a292))
% 0.59/0.76  ((a344) != (a283))
% 0.59/0.76  ((a311) != (a310))
% 0.59/0.76  ((a330) != (a336))
% 0.59/0.76  ((a300) != (a306))
% 0.59/0.76  ((a322) != zenon_X22)
% 0.59/0.76  ((a285) != (a300))
% 0.59/0.76  (c0_1 (a291))
% 0.59/0.76  (zenon_X10 != (a333))
% 0.59/0.76  ((a311) != (a337))
% 0.59/0.76  ((a340) != (a297))
% 0.59/0.76  ((a315) != (a317))
% 0.59/0.76  ((a285) != (a311))
% 0.59/0.76  ((a330) != (a326))
% 0.59/0.76  ((a304) != (a291))
% 0.59/0.76  ((a311) != (a334))
% 0.59/0.76  ((a343) != (a327))
% 0.59/0.76  (c2_1 (a345))
% 0.59/0.76  ((a317) != (a327))
% 0.59/0.76  ((a299) != (a337))
% 0.59/0.76  ((a342) != (a307))
% 0.59/0.76  ((a297) != (a306))
% 0.59/0.76  ((a319) != (a322))
% 0.59/0.76  ((a311) != (a324))
% 0.59/0.76  (-. (c0_1 (a318)))
% 0.59/0.76  ((a287) != (a336))
% 0.59/0.76  ((a331) != (a297))
% 0.59/0.76  ((a315) != (a340))
% 0.59/0.76  (c2_1 (a340))
% 0.59/0.76  ((a345) != (a344))
% 0.59/0.76  ((a317) != (a310))
% 0.59/0.76  (hskp22)
% 0.59/0.76  ((a330) != (a310))
% 0.59/0.76  ((a340) != (a313))
% 0.59/0.76  ((a287) != (a290))
% 0.59/0.76  ((a345) != (a342))
% 0.59/0.76  ((a315) != (a288))
% 0.59/0.76  ((a286) != (a313))
% 0.59/0.76  (-. (c1_1 (a288)))
% 0.59/0.76  ((a317) != (a340))
% 0.59/0.76  (hskp5)
% 0.59/0.76  ((a319) != (a336))
% 0.59/0.76  ((a299) != (a335))
% 0.59/0.76  ((a304) != zenon_X22)
% 0.59/0.76  ((a317) != (a298))
% 0.59/0.76  ((a286) != (a319))
% 0.59/0.76  ((a335) != (a297))
% 0.59/0.76  ((a304) != (a335))
% 0.59/0.76  ((a293) != zenon_X22)
% 0.59/0.76  ((a326) != (a324))
% 0.59/0.76  ((a299) != (a300))
% 0.59/0.76  ((a333) != (a326))
% 0.59/0.76  ((a298) != (a291))
% 0.59/0.76  ((a335) != (a326))
% 0.59/0.76  ((a334) != (a318))
% 0.59/0.76  ((a301) != (a327))
% 0.59/0.76  ((a284) != (a310))
% 0.59/0.76  ((a331) != (a306))
% 0.59/0.76  ((a336) != (a316))
% 0.59/0.76  ((a304) != (a290))
% 0.59/0.76  ((a331) != (a290))
% 0.59/0.76  ((a289) != (a337))
% 0.59/0.76  ((a326) != zenon_X22)
% 0.59/0.76  (c2_1 zenon_X22)
% 0.59/0.76  ((a287) != (a296))
% 0.59/0.76  ((a303) != (a337))
% 0.59/0.76  ((a304) != (a305))
% 0.59/0.76  ((a282) != (a330))
% 0.59/0.76  ((a297) != (a318))
% 0.59/0.76  ((a285) != (a319))
% 0.59/0.76  ((a327) != (a298))
% 0.59/0.76  (c0_1 (a289))
% 0.59/0.76  ((a311) != zenon_X22)
% 0.59/0.76  ((a302) != (a333))
% 0.59/0.76  ((a304) != (a310))
% 0.59/0.76  ((a331) != (a325))
% 0.59/0.76  (-. (c3_1 (a345)))
% 0.59/0.76  ((a287) != (a319))
% 0.59/0.76  ((a327) != (a294))
% 0.59/0.76  ((a296) != (a292))
% 0.59/0.76  (c0_1 (a285))
% 0.59/0.76  ((a330) != (a284))
% 0.59/0.76  (c0_1 (a316))
% 0.59/0.76  ((a282) != (a337))
% 0.59/0.76  ((a345) != (a305))
% 0.59/0.76  ((a300) != (a327))
% 0.59/0.76  ((a331) != (a336))
% 0.59/0.76  ((a287) != (a306))
% 0.59/0.76  ((a288) != (a306))
% 0.59/0.76  ((a301) != (a294))
% 0.59/0.76  ((a335) != (a286))
% 0.59/0.76  ((a326) != (a292))
% 0.59/0.76  (zenon_X20 != (a316))
% 0.59/0.76  ((a299) != (a347))
% 0.59/0.76  (-. (c0_1 (a286)))
% 0.59/0.76  ((a343) != (a288))
% 0.59/0.76  (zenon_X10 != (a324))
% 0.59/0.76  ((a282) != (a312))
% 0.59/0.76  ((a284) != (a292))
% 0.59/0.76  ((a303) != (a304))
% 0.59/0.76  (-. (c3_1 (a337)))
% 0.59/0.76  (c2_1 (a315))
% 0.59/0.76  ((a287) != (a300))
% 0.59/0.76  ((a345) != (a282))
% 0.59/0.76  ((a325) != (a283))
% 0.59/0.76  ((a316) != (a286))
% 0.59/0.76  ((a288) != (a337))
% 0.59/0.76  (c1_1 (a335))
% 0.59/0.76  (hskp34)
% 0.59/0.76  ((a298) != (a312))
% 0.59/0.76  ((a334) != (a335))
% 0.59/0.76  ((a299) != (a318))
% 0.59/0.76  ((a340) != (a347))
% 0.59/0.76  ((a287) != (a283))
% 0.59/0.76  ((a283) != (a313))
% 0.59/0.76  ((a285) != (a336))
% 0.59/0.76  ((a285) != (a318))
% 0.59/0.76  ((a334) != (a336))
% 0.59/0.76  (zenon_X0 != (a286))
% 0.59/0.76  ((a325) != (a316))
% 0.59/0.76  (-. (c2_1 (a336)))
% 0.59/0.76  (c3_1 (a309))
% 0.59/0.76  ((a283) != (a336))
% 0.59/0.76  ((a296) != (a310))
% 0.59/0.76  ((a285) != (a335))
% 0.59/0.76  ((a313) != (a306))
% 0.59/0.76  (c3_1 (a327))
% 0.59/0.76  ((a325) != (a305))
% 0.59/0.76  (zenon_X10 != (a293))
% 0.59/0.76  ((a316) != (a306))
% 0.59/0.76  (zenon_X22 != (a310))
% 0.59/0.76  ((a284) != (a282))
% 0.59/0.76  ((a331) != (a324))
% 0.59/0.76  ((a343) != (a331))
% 0.59/0.76  ((a325) != (a326))
% 0.59/0.76  (zenon_X22 != (a306))
% 0.59/0.76  (zenon_X22 != (a312))
% 0.59/0.76  ((a316) != (a290))
% 0.59/0.76  ((a340) != (a300))
% 0.59/0.76  (-. (c1_1 (a336)))
% 0.59/0.76  ((a313) != (a301))
% 0.59/0.76  ((a302) != (a319))
% 0.59/0.76  ((a313) != (a311))
% 0.59/0.76  ((a293) != (a344))
% 0.59/0.76  ((a345) != (a312))
% 0.59/0.76  (zenon_X10 != (a300))
% 0.59/0.76  ((a327) != (a290))
% 0.59/0.76  (c3_1 (a300))
% 0.59/0.76  ((a342) != (a316))
% 0.59/0.76  ((a315) != (a336))
% 0.59/0.76  ((a340) != (a322))
% 0.59/0.76  (zenon_X20 != (a296))
% 0.59/0.76  ((a282) != (a318))
% 0.59/0.76  ((a304) != (a312))
% 0.59/0.76  ((a325) != (a301))
% 0.59/0.76  ((a297) != (a312))
% 0.59/0.76  ((a285) != (a306))
% 0.59/0.76  ((a330) != (a334))
% 0.59/0.76  ((a345) != (a337))
% 0.59/0.76  (c1_1 (a293))
% 0.59/0.76  ((a331) != (a293))
% 0.59/0.76  ((a288) != (a330))
% 0.59/0.76  ((a317) != (a301))
% 0.59/0.76  ((a285) != (a333))
% 0.59/0.76  ((a315) != (a305))
% 0.59/0.76  ((a287) != (a331))
% 0.59/0.76  (c3_1 (a289))
% 0.59/0.76  (-. (c2_1 (a319)))
% 0.59/0.76  ((a282) != (a305))
% 0.59/0.76  ((a343) != (a326))
% 0.59/0.76  (-. (c3_1 (a316)))
% 0.59/0.76  ((a299) != (a291))
% 0.59/0.76  ((a309) != (a344))
% 0.59/0.76  ((a311) != (a318))
% 0.59/0.76  (c2_1 (a307))
% 0.59/0.76  ((a285) != (a312))
% 0.59/0.76  ((a342) != (a294))
% 0.59/0.76  ((a345) != (a293))
% 0.59/0.76  ((a294) != (a310))
% 0.59/0.76  ((a340) != (a316))
% 0.59/0.76  (-. (c3_1 (a340)))
% 0.59/0.76  ((a326) != (a337))
% 0.59/0.76  ((a299) != (a307))
% 0.59/0.76  ((a325) != (a282))
% 0.59/0.76  ((a291) != (a290))
% 0.59/0.76  ((a343) != (a317))
% 0.59/0.76  ((a297) != (a288))
% 0.59/0.76  ((a302) != (a299))
% 0.59/0.76  ((a284) != (a312))
% 0.59/0.76  (-. (c1_1 (a290)))
% 0.59/0.76  ((a284) != (a306))
% 0.59/0.76  ((a297) != (a313))
% 0.59/0.76  ((a289) != (a333))
% 0.59/0.76  ((a298) != (a322))
% 0.59/0.76  ((a343) != (a294))
% 0.59/0.76  ((a298) != (a333))
% 0.59/0.76  ((a335) != (a283))
% 0.59/0.76  (-. (c0_1 (a319)))
% 0.59/0.76  (c0_1 (a304))
% 0.59/0.76  ((a342) != (a292))
% 0.59/0.76  ((a311) != (a331))
% 0.59/0.76  (-. (c0_1 (a310)))
% 0.59/0.76  ((a304) != (a324))
% 0.59/0.76  ((a313) != (a290))
% 0.59/0.76  (-. (c3_1 (a333)))
% 0.59/0.76  ((a305) != (a284))
% 0.59/0.76  ((a305) != (a347))
% 0.59/0.76  ((a334) != (a325))
% 0.59/0.76  (c2_1 (a284))
% 0.59/0.76  ((a297) != (a327))
% 0.59/0.76  ((a333) != (a347))
% 0.59/0.76  ((a296) != (a288))
% 0.59/0.76  ((a305) != (a290))
% 0.59/0.76  ((a285) != (a298))
% 0.59/0.76  ((a288) != (a283))
% 0.59/0.76  ((a315) != (a342))
% 0.59/0.76  ((a344) != (a324))
% 0.59/0.76  ((a330) != (a298))
% 0.59/0.76  (zenon_X10 != (a336))
% 0.59/0.76  ((a288) != (a310))
% 0.59/0.76  ((a304) != (a292))
% 0.59/0.76  ((a330) != (a305))
% 0.59/0.76  ((a304) != (a318))
% 0.59/0.76  ((a335) != (a322))
% 0.59/0.76  ((a283) != (a300))
% 0.59/0.76  ((a319) != (a290))
% 0.59/0.76  ((a342) != zenon_X22)
% 0.59/0.76  ((a297) != (a284))
% 0.59/0.76  (c0_1 (a342))
% 0.59/0.76  ((a303) != (a293))
% 0.59/0.76  ((a334) != (a312))
% 0.59/0.76  (-. (c1_1 (a347)))
% 0.59/0.76  ((a313) != (a342))
% 0.59/0.76  ((a344) != (a290))
% 0.59/0.76  ((a342) != (a286))
% 0.59/0.76  (c1_1 (a303))
% 0.59/0.76  ((a304) != (a298))
% 0.59/0.76  ((a286) != (a326))
% 0.59/0.76  ((a289) != (a319))
% 0.59/0.76  ((a342) != (a327))
% 0.59/0.76  (-. (c1_1 (a344)))
% 0.59/0.76  ((a293) != (a327))
% 0.59/0.76  ((a296) != (a311))
% 0.59/0.76  ((a313) != (a305))
% 0.59/0.76  ((a307) != (a290))
% 0.59/0.76  ((a287) != (a335))
% 0.59/0.76  (c3_1 (a288))
% 0.59/0.76  ((a297) != (a322))
% 0.59/0.76  (c1_1 (a307))
% 0.59/0.76  ((a299) != (a286))
% 0.59/0.76  ((a291) != (a319))
% 0.59/0.76  ((a345) != (a297))
% 0.59/0.76  (c0_1 (a326))
% 0.59/0.76  (hskp42)
% 0.59/0.76  (c2_1 (a316))
% 0.59/0.76  ((a289) != (a306))
% 0.59/0.76  ((a333) != (a292))
% 0.59/0.76  ((a326) != (a312))
% 0.59/0.76  ((a302) != (a306))
% 0.59/0.76  ((a340) != (a306))
% 0.59/0.76  ((a302) != (a286))
% 0.59/0.76  ((a285) != (a344))
% 0.59/0.76  ((a345) != (a304))
% 0.59/0.76  ((a302) != (a291))
% 0.59/0.76  ((a327) != (a331))
% 0.59/0.76  ((a334) != (a304))
% 0.59/0.76  (-. (c1_1 (a306)))
% 0.59/0.76  ((a291) != (a301))
% 0.59/0.76  (-. (c1_1 (a311)))
% 0.59/0.76  ((a331) != (a294))
% 0.59/0.76  ((a335) != (a336))
% 0.59/0.76  ((a299) != (a333))
% 0.59/0.76  ((a285) != (a297))
% 0.59/0.76  (hskp24)
% 0.59/0.76  ((a296) != (a293))
% 0.59/0.76  (-. (c1_1 (a322)))
% 0.59/0.76  ((a284) != (a324))
% 0.59/0.76  ((a296) != (a322))
% 0.59/0.76  ((a305) != (a327))
% 0.59/0.76  ((a293) != (a319))
% 0.59/0.76  ((a334) != (a347))
% 0.59/0.76  (zenon_X0 != (a301))
% 0.59/0.76  (zenon_X10 != (a304))
% 0.59/0.76  ((a333) != (a300))
% 0.59/0.76  ((a317) != (a344))
% 0.59/0.76  ((a330) != (a319))
% 0.59/0.76  ((a296) != (a336))
% 0.59/0.76  ((a299) != (a322))
% 0.59/0.76  ((a303) != (a334))
% 0.59/0.76  (c0_1 (a343))
% 0.59/0.76  ((a325) != (a330))
% 0.59/0.76  ((a331) != (a305))
% 0.59/0.76  (c3_1 (a282))
% 0.59/0.76  (zenon_X20 != (a310))
% 0.59/0.76  ((a282) != (a291))
% 0.59/0.76  ((a284) != (a309))
% 0.59/0.76  ((a319) != (a344))
% 0.59/0.76  (-. (c3_1 zenon_X22))
% 0.59/0.76  (zenon_X0 != (a333))
% 0.59/0.76  (zenon_X22 != (a335))
% 0.59/0.76  ((a304) != (a322))
% 0.59/0.76  ((a293) != (a291))
% 0.59/0.76  ((a298) != (a324))
% 0.59/0.76  ((a342) != (a337))
% 0.59/0.76  ((a285) != (a301))
% 0.59/0.76  (zenon_X22 != (a337))
% 0.59/0.76  (c2_1 (a283))
% 0.59/0.76  ((a343) != (a291))
% 0.59/0.76  ((a335) != (a316))
% 0.59/0.76  (zenon_X10 != (a335))
% 0.59/0.76  ((a286) != (a300))
% 0.59/0.76  ((a344) != (a334))
% 0.59/0.76  ((a309) != (a322))
% 0.59/0.76  ((a340) != (a324))
% 0.59/0.76  ((a345) != (a322))
% 0.59/0.76  ((a305) != (a312))
% 0.59/0.76  ((a303) != (a322))
% 0.59/0.76  ((a296) != (a337))
% 0.59/0.76  ((a334) != (a309))
% 0.59/0.76  ((a282) != (a294))
% 0.59/0.76  ((a343) != (a296))
% 0.59/0.76  ((a302) != (a316))
% 0.59/0.76  (zenon_X20 != (a318))
% 0.59/0.76  ((a301) != (a311))
% 0.59/0.76  ((a282) != (a301))
% 0.59/0.76  ((a283) != (a310))
% 0.59/0.76  ((a294) != (a313))
% 0.59/0.76  ((a345) != (a291))
% 0.59/0.76  ((a298) != (a306))
% 0.59/0.76  ((a334) != (a313))
% 0.59/0.76  ((a300) != (a290))
% 0.59/0.76  ((a304) != (a283))
% 0.59/0.76  ((a287) != (a333))
% 0.59/0.76  ((a344) != (a301))
% 0.59/0.76  (-. (c1_1 (a294)))
% 0.59/0.76  (hskp13)
% 0.59/0.76  ((a313) != (a333))
% 0.59/0.76  ((a343) != (a336))
% 0.59/0.76  (zenon_X20 != (a284))
% 0.59/0.76  (c0_1 (a300))
% 0.59/0.76  ((a284) != (a337))
% 0.59/0.76  ((a297) != (a298))
% 0.59/0.76  ((a297) != (a326))
% 0.59/0.76  ((a307) != (a337))
% 0.59/0.76  ((a284) != (a326))
% 0.59/0.76  (-. (c1_1 (a300)))
% 0.59/0.76  ((a325) != (a327))
% 0.59/0.76  (c2_1 (a303))
% 0.59/0.76  ((a343) != (a299))
% 0.59/0.76  ((a319) != (a282))
% 0.59/0.76  ((a289) != (a296))
% 0.59/0.76  ((a283) != (a306))
% 0.59/0.76  ((a287) != zenon_X22)
% 0.59/0.76  ((a307) != (a317))
% 0.59/0.76  ((a282) != (a299))
% 0.59/0.76  ((a299) != (a313))
% 0.59/0.76  ((a322) != (a290))
% 0.59/0.76  ((a299) != (a284))
% 0.59/0.76  ((a284) != (a335))
% 0.59/0.76  ((a340) != (a286))
% 0.59/0.76  ((a345) != (a292))
% 0.59/0.76  (c0_1 (a344))
% 0.59/0.76  ((a303) != (a283))
% 0.59/0.76  ((a327) != (a286))
% 0.59/0.76  ((a313) != (a324))
% 0.59/0.76  ((a315) != (a311))
% 0.59/0.76  (-. (c2_1 (a326)))
% 0.59/0.76  ((a300) != (a324))
% 0.59/0.76  ((a331) != (a292))
% 0.59/0.76  ((a317) != (a347))
% 0.59/0.76  (c3_1 (a302))
% 0.59/0.76  (c3_1 (a325))
% 0.59/0.76  ((a291) != zenon_X22)
% 0.59/0.76  ((a294) != (a306))
% 0.59/0.76  ((a302) != (a347))
% 0.59/0.76  (hskp18)
% 0.59/0.76  ((a315) != (a286))
% 0.59/0.76  ((a296) != (a300))
% 0.59/0.76  ((a284) != (a325))
% 0.59/0.76  (zenon_X0 != (a335))
% 0.59/0.76  ((a315) != (a310))
% 0.59/0.76  (zenon_X20 != (a319))
% 0.59/0.76  ((a313) != (a288))
% 0.59/0.76  ((a282) != (a286))
% 0.59/0.76  (c2_1 (a282))
% 0.59/0.76  ((a344) != (a340))
% 0.59/0.76  ((a325) != (a290))
% 0.59/0.76  ((a303) != (a318))
% 0.59/0.76  ((a304) != (a288))
% 0.59/0.76  (zenon_X10 != (a317))
% 0.59/0.76  ((a342) != (a319))
% 0.59/0.76  ((a285) != (a345))
% 0.59/0.76  ((a288) != (a299))
% 0.59/0.76  ((a307) != (a306))
% 0.59/0.76  ((a311) != (a327))
% 0.59/0.76  ((a289) != (a283))
% 0.59/0.76  ((a344) != (a286))
% 0.59/0.76  (-. (c1_1 (a305)))
% 0.59/0.76  ((a311) != (a283))
% 0.59/0.76  ((a302) != (a288))
% 0.59/0.76  ((a293) != (a317))
% 0.59/0.76  ((a304) != (a342))
% 0.59/0.76  (hskp7)
% 0.59/0.76  ((a291) != (a324))
% 0.59/0.76  ((a299) != (a326))
% 0.59/0.76  ((a301) != (a326))
% 0.59/0.76  ((a294) != (a293))
% 0.59/0.76  ((a285) != (a325))
% 0.59/0.76  ((a289) != (a331))
% 0.59/0.76  ((a291) != (a347))
% 0.59/0.76  ((a313) != (a310))
% 0.59/0.76  ((a304) != (a297))
% 0.59/0.76  ((a300) != zenon_X22)
% 0.59/0.76  (-. (c2_1 (a304)))
% 0.59/0.76  ((a284) != (a327))
% 0.59/0.76  ((a342) != (a334))
% 0.59/0.76  ((a315) != (a292))
% 0.59/0.76  ((a287) != (a299))
% 0.59/0.76  ((a303) != (a311))
% 0.59/0.76  ((a335) != (a292))
% 0.59/0.76  ((a296) != (a326))
% 0.59/0.76  ((a307) != (a294))
% 0.59/0.76  ((a301) != (a290))
% 0.59/0.76  ((a309) != (a300))
% 0.59/0.76  ((a303) != (a317))
% 0.59/0.76  ((a330) != (a312))
% 0.59/0.76  ((a313) != (a330))
% 0.59/0.76  ((a342) != (a290))
% 0.59/0.76  ((a299) != (a304))
% 0.59/0.76  ((a291) != (a310))
% 0.59/0.76  ((a287) != (a317))
% 0.59/0.76  ((a317) != (a306))
% 0.59/0.76  ((a283) != (a337))
% 0.59/0.76  (zenon_X10 != (a326))
% 0.59/0.76  (zenon_X10 != (a327))
% 0.59/0.76  ((a343) != (a310))
% 0.59/0.76  ((a285) != (a313))
% 0.59/0.76  ((a289) != (a291))
% 0.59/0.76  ((a343) != (a298))
% 0.59/0.76  ((a309) != (a317))
% 0.59/0.76  ((a317) != (a333))
% 0.59/0.76  ((a289) != (a325))
% 0.59/0.76  ((a287) != (a310))
% 0.59/0.76  ((a283) != (a326))
% 0.59/0.76  ((a286) != (a310))
% 0.59/0.76  ((a313) != (a316))
% 0.59/0.76  ((a297) != (a309))
% 0.59/0.76  (-. (c2_1 (a309)))
% 0.59/0.76  ((a309) != zenon_X22)
% 0.59/0.76  ((a304) != (a311))
% 0.59/0.76  ((a315) != (a327))
% 0.59/0.76  ((a284) != (a336))
% 0.59/0.76  ((a317) != (a288))
% 0.59/0.76  ((a289) != (a284))
% 0.59/0.76  (-. (c2_1 (a313)))
% 0.59/0.76  ((a296) != (a327))
% 0.59/0.76  ((a345) != (a306))
% 0.59/0.76  ((a296) != (a335))
% 0.59/0.76  (c3_1 (a315))
% 0.59/0.76  ((a345) != (a316))
% 0.59/0.76  (c1_1 (a340))
% 0.59/0.76  (-. (c0_1 (a312)))
% 0.59/0.76  (-. (c3_1 (a296)))
% 0.59/0.76  ((a302) != (a345))
% 0.59/0.76  ((a282) != (a283))
% 0.59/0.76  ((a303) != (a284))
% 0.59/0.76  ((a283) != (a305))
% 0.59/0.76  (c2_1 (a334))
% 0.59/0.76  ((a327) != (a306))
% 0.59/0.76  (-. (c2_1 (a322)))
% 0.59/0.76  ((a317) != zenon_X22)
% 0.59/0.76  ((a282) != (a336))
% 0.59/0.76  ((a289) != (a292))
% 0.59/0.76  ((a299) != (a305))
% 0.59/0.76  ((a325) != (a297))
% 0.59/0.76  (c0_1 (a293))
% 0.59/0.76  (-. (c3_1 (a298)))
% 0.59/0.76  (hskp51)
% 0.59/0.76  ((a289) != (a317))
% 0.59/0.76  ((a293) != (a310))
% 0.59/0.76  (-. (c3_1 (a292)))
% 0.59/0.76  ((a299) != (a298))
% 0.59/0.76  ((a335) != (a327))
% 0.59/0.76  ((a340) != (a309))
% 0.59/0.76  ((a288) != (a301))
% 0.59/0.76  ((a297) != (a293))
% 0.59/0.76  ((a303) != (a335))
% 0.59/0.76  (c2_1 (a299))
% 0.59/0.76  ((a311) != (a330))
% 0.59/0.76  ((a303) != (a291))
% 0.59/0.76  ((a303) != (a305))
% 0.59/0.76  ((a330) != (a306))
% 0.59/0.76  ((a345) != (a319))
% 0.59/0.76  (zenon_X10 != (a312))
% 0.59/0.76  ((a345) != (a286))
% 0.59/0.76  ((a313) != (a327))
% 0.59/0.76  ((a304) != (a337))
% 0.59/0.76  ((a307) != (a286))
% 0.59/0.76  ((a343) != (a345))
% 0.59/0.76  (-. (c1_1 (a326)))
% 0.59/0.76  (zenon_X0 != (a319))
% 0.59/0.76  ((a294) != (a322))
% 0.59/0.76  ((a331) != (a313))
% 0.59/0.76  ((a345) != (a290))
% 0.59/0.76  ((a299) != (a319))
% 0.59/0.76  ((a340) != (a304))
% 0.59/0.76  (c1_1 (a319))
% 0.59/0.76  ((a284) != (a290))
% 0.59/0.76  ((a304) != (a294))
% 0.59/0.76  ((a313) != (a347))
% 0.59/0.76  (c3_1 (a344))
% 0.59/0.76  (zenon_X20 != (a286))
% 0.59/0.76  (c1_1 (a313))
% 0.59/0.76  ((a315) != (a297))
% 0.59/0.76  ((a344) != (a310))
% 0.59/0.76  ((a343) != (a290))
% 0.59/0.76  ((a345) != (a336))
% 0.59/0.76  (zenon_X20 != (a317))
% 0.59/0.76  (-. (c1_1 (a283)))
% 0.59/0.76  (-. (c3_1 (a312)))
% 0.59/0.76  ((a302) != (a297))
% 0.59/0.76  ((a304) != (a336))
% 0.59/0.76  ((a325) != (a318))
% 0.59/0.76  ((a300) != (a316))
% 0.59/0.76  (c1_1 (a304))
% 0.59/0.76  ((a317) != (a324))
% 0.59/0.76  (c1_1 (a284))
% 0.59/0.76  ((a333) != (a291))
% 0.59/0.76  ((a331) != (a322))
% 0.59/0.76  (zenon_X0 != (a292))
% 0.59/0.76  ((a298) != (a309))
% 0.59/0.76  ((a289) != (a335))
% 0.59/0.76  ((a340) != (a305))
% 0.59/0.76  ((a300) != (a312))
% 0.59/0.76  ((a317) != (a290))
% 0.59/0.76  ((a304) != (a317))
% 0.59/0.76  ((a311) != (a286))
% 0.59/0.76  ((a327) != zenon_X22)
% 0.59/0.76  ((a313) != (a326))
% 0.59/0.76  ((a287) != (a347))
% 0.59/0.76  (c3_1 (a311))
% 0.59/0.76  ((a285) != (a310))
% 0.59/0.76  (c0_1 (a305))
% 0.59/0.76  ((a288) != (a290))
% 0.59/0.76  ((a315) != (a324))
% 0.59/0.76  ((a304) != (a344))
% 0.59/0.76  (-. (c2_1 (a300)))
% 0.59/0.76  ((a303) != (a310))
% 0.59/0.76  (c3_1 (a342))
% 0.59/0.76  (-. (c2_1 (a318)))
% 0.59/0.76  ((a287) != (a330))
% 0.59/0.76  ((a307) != (a291))
% 0.59/0.76  ((a287) != (a284))
% 0.59/0.76  ((a289) != (a330))
% 0.59/0.76  (-. (c0_1 (a284)))
% 0.59/0.76  ((a286) != (a322))
% 0.59/0.76  (-. (c3_1 (a290)))
% 0.59/0.76  ((a317) != (a336))
% 0.59/0.76  ((a309) != (a333))
% 0.59/0.76  (hskp36)
% 0.59/0.76  (-. (c0_1 (a298)))
% 0.59/0.76  ((a293) != (a326))
% 0.59/0.76  (c0_1 zenon_X20)
% 0.59/0.76  (c2_1 (a286))
% 0.59/0.76  ((a296) != (a294))
% 0.59/0.76  (zenon_X20 != (a334))
% 0.59/0.76  ((a287) != (a305))
% 0.59/0.76  ((a282) != (a334))
% 0.59/0.76  ((a345) != (a310))
% 0.59/0.76  ((a283) != (a312))
% 0.59/0.76  ((a283) != (a291))
% 0.59/0.76  ((a319) != (a327))
% 0.59/0.76  ((a288) != (a333))
% 0.59/0.76  (hskp8)
% 0.59/0.76  ((a299) != (a312))
% 0.59/0.76  ((a285) != (a324))
% 0.59/0.76  ((a293) != (a322))
% 0.59/0.76  ((a342) != (a312))
% 0.59/0.76  ((a309) != (a290))
% 0.59/0.76  ((a307) != (a318))
% 0.59/0.76  (zenon_X22 != (a347))
% 0.59/0.76  ((a294) != (a336))
% 0.59/0.76  ((a285) != (a292))
% 0.59/0.76  ((a287) != (a337))
% 0.59/0.76  ((a299) != (a306))
% 0.59/0.76  ((a293) != (a342))
% 0.59/0.76  ((a316) != (a347))
% 0.59/0.76  (-. (c2_1 (a288)))
% 0.59/0.76  ((a288) != (a324))
% 0.59/0.76  ((a330) != (a304))
% 0.59/0.76  (c3_1 (a317))
% 0.59/0.76  ((a343) != (a318))
% 0.59/0.76  (-. (c0_1 (a335)))
% 0.59/0.76  ((a333) != (a305))
% 0.59/0.76  ((a330) != (a300))
% 0.59/0.76  ((a345) != (a300))
% 0.59/0.76  ((a344) != (a347))
% 0.59/0.76  (-. (c0_1 (a301)))
% 0.59/0.76  ((a325) != (a298))
% 0.59/0.76  (-. (c2_1 (a325)))
% 0.59/0.76  ((a331) != (a304))
% 0.59/0.76  ((a325) != (a310))
% 0.59/0.76  ((a316) != (a298))
% 0.59/0.76  ((a315) != (a313))
% 0.59/0.76  ((a325) != (a336))
% 0.59/0.76  (hskp26)
% 0.59/0.76  ((a297) != (a300))
% 0.59/0.76  ((a283) != (a322))
% 0.59/0.76  (c1_1 (a296))
% 0.59/0.76  ((a285) != (a316))
% 0.59/0.76  ((a334) != (a288))
% 0.59/0.76  ((a336) != (a327))
% 0.59/0.76  ((a304) != (a326))
% 0.59/0.76  ((a319) != (a294))
% 0.59/0.76  ((a345) != (a317))
% 0.59/0.76  ((a307) != (a347))
% 0.59/0.76  ((a322) != (a316))
% 0.59/0.76  (zenon_X10 != (a288))
% 0.59/0.76  ((a316) != (a292))
% 0.59/0.76  ((a301) != (a336))
% 0.59/0.76  ((a340) != (a292))
% 0.59/0.76  ((a296) != (a347))
% 0.59/0.76  ((a309) != (a318))
% 0.59/0.76  ((a325) != (a291))
% 0.59/0.76  ((a342) != (a306))
% 0.59/0.76  ((a282) != (a292))
% 0.59/0.76  ((a336) != (a292))
% 0.59/0.76  ((a298) != (a336))
% 0.59/0.76  ((a331) != (a309))
% 0.59/0.76  ((a294) != (a333))
% 0.59/0.76  (-. (c3_1 (a283)))
% 0.59/0.76  ((a289) != zenon_X22)
% 0.59/0.76  ((a301) != (a292))
% 0.59/0.76  ((a286) != (a306))
% 0.59/0.76  ((a286) != (a312))
% 0.59/0.76  (zenon_X0 != (a334))
% 0.59/0.76  ((a317) != (a283))
% 0.59/0.76  ((a293) != (a300))
% 0.59/0.76  ((a289) != (a340))
% 0.59/0.76  ((a325) != (a288))
% 0.59/0.76  ((a303) != (a319))
% 0.59/0.76  ((a307) != (a311))
% 0.59/0.76  ((a287) != (a312))
% 0.59/0.76  ((a344) != (a299))
% 0.59/0.76  ((a315) != (a294))
% 0.59/0.76  ((a284) != (a319))
% 0.59/0.76  ((a303) != (a297))
% 0.59/0.76  ((a303) != (a301))
% 0.59/0.76  (zenon_X20 != (a306))
% 0.59/0.76  ((a297) != (a290))
% 0.59/0.76  ((a304) != (a286))
% 0.59/0.76  ((a303) != (a290))
% 0.59/0.76  ((a289) != (a326))
% 0.59/0.76  ((a293) != (a347))
% 0.59/0.76  ((a293) != (a305))
% 0.59/0.76  ((a343) != (a330))
% 0.59/0.76  ((a305) != (a316))
% 0.59/0.76  (zenon_X10 != (a309))
% 0.59/0.76  ((a309) != (a326))
% 0.59/0.76  ((a343) != (a300))
% 0.59/0.76  (c1_1 (a309))
% 0.59/0.76  ((a309) != (a319))
% 0.59/0.76  ((a315) != (a316))
% 0.59/0.76  ((a302) != (a330))
% 0.59/0.76  ((a293) != (a333))
% 0.59/0.76  (zenon_X10 != (a337))
% 0.59/0.76  ((a289) != (a298))
% 0.59/0.76  ((a302) != (a310))
% 0.59/0.76  ((a344) != (a337))
% 0.59/0.76  ((a302) != (a290))
% 0.59/0.76  ((a315) != (a318))
% 0.59/0.76  ((a340) != (a291))
% 0.59/0.76  (zenon_X0 != (a284))
% 0.59/0.76  ((a289) != (a286))
% 0.59/0.76  ((a289) != (a304))
% 0.59/0.76  ((a289) != (a316))
% 0.59/0.76  ((a330) != (a335))
% 0.59/0.76  ((a343) != (a324))
% 0.59/0.76  ((a289) != (a322))
% 0.59/0.76  ((a297) != (a324))
% 0.59/0.76  ((a335) != (a290))
% 0.59/0.76  (c3_1 zenon_X20)
% 0.59/0.76  ((a305) != (a306))
% 0.59/0.76  (-. (c0_1 (a337)))
% 0.59/0.76  ((a282) != (a322))
% 0.59/0.76  ((a287) != (a294))
% 0.59/0.76  ((a345) != (a325))
% 0.59/0.76  ((a307) != (a283))
% 0.59/0.76  (c2_1 (a294))
% 0.59/0.76  ((a304) != (a284))
% 0.59/0.76  ((a340) != (a312))
% 0.59/0.76  ((a302) != (a296))
% 0.59/0.76  ((a286) != (a324))
% 0.59/0.76  ((a317) != (a322))
% 0.59/0.76  ((a298) != (a318))
% 0.59/0.76  (zenon_X0 != (a312))
% 0.59/0.76  ((a303) != (a342))
% 0.59/0.76  ((a282) != (a293))
% 0.59/0.76  ((a340) != (a294))
% 0.59/0.76  ((a303) != (a312))
% 0.59/0.76  ((a345) != (a327))
% 0.59/0.76  ((a309) != (a311))
% 0.59/0.76  (zenon_X10 != (a318))
% 0.59/0.76  ((a333) != (a310))
% 0.59/0.76  (c1_1 (a325))
% 0.59/0.76  (zenon_X0 != (a347))
% 0.59/0.76  (zenon_X0 != (a298))
% 0.59/0.76  ((a300) != (a318))
% 0.59/0.76  ((a302) != (a301))
% 0.59/0.76  ((a303) != (a333))
% 0.59/0.76  (-. (c3_1 (a306)))
% 0.59/0.76  ((a302) != (a292))
% 0.59/0.76  (c1_1 (a343))
% 0.59/0.76  ((a311) != (a333))
% 0.59/0.76  ((a304) != (a347))
% 0.59/0.76  ((a340) != (a337))
% 0.59/0.76  ((a331) != (a342))
% 0.59/0.76  ((a317) != (a312))
% 0.59/0.76  ((a284) != (a347))
% 0.59/0.76  ((a322) != (a330))
% 0.59/0.76  ((a303) != (a327))
% 0.59/0.76  (-. (c0_1 (a292)))
% 0.59/0.76  ((a282) != (a300))
% 0.59/0.76  ((a322) != (a312))
% 0.59/0.76  ((a315) != (a333))
% 0.59/0.76  (zenon_X10 != (a313))
% 0.59/0.76  ((a322) != (a337))
% 0.59/0.76  ((a296) != (a333))
% 0.59/0.76  ((a343) != (a311))
% 0.59/0.76  (c1_1 (a333))
% 0.59/0.76  ((a313) != zenon_X22)
% 0.59/0.76  (c2_1 (a289))
% 0.59/0.76  ((a315) != (a284))
% 0.59/0.76  ((a303) != (a316))
% 0.59/0.76  (zenon_X20 != (a333))
% 0.59/0.76  ((a302) != zenon_X22)
% 0.59/0.76  ((a326) != (a327))
% 0.59/0.76  ((a298) != (a337))
% 0.59/0.76  ((a282) != (a326))
% 0.59/0.76  (-. (c3_1 (a331)))
% 0.59/0.76  ((a330) != (a347))
% 0.59/0.76  ((a289) != (a301))
% 0.59/0.76  ((a340) != (a318))
% 0.59/0.76  (ndr1_0)
% 0.59/0.76  ((a289) != (a336))
% 0.59/0.76  ((a297) != (a333))
% 0.59/0.76  (hskp2)
% 0.59/0.76  ((a284) != (a333))
% 0.59/0.76  ((a299) != (a292))
% 0.59/0.76  ((a289) != (a288))
% 0.59/0.76  ((a307) != (a282))
% 0.59/0.76  ((a315) != (a335))
% 0.59/0.76  ((a309) != (a292))
% 0.59/0.76  ((a327) != (a318))
% 0.59/0.76  ((a287) != (a316))
% 0.59/0.76  ((a293) != (a311))
% 0.59/0.76  ((a287) != (a301))
% 0.59/0.76  (c3_1 (a322))
% 0.59/0.76  (zenon_X0 != (a324))
% 0.59/0.76  (zenon_X10 != (a310))
% 0.59/0.76  ((a285) != (a288))
% 0.59/0.76  ((a293) != (a324))
% 0.59/0.76  ((a311) != (a347))
% 0.59/0.76  ((a302) != (a326))
% 0.59/0.76  ((a315) != (a298))
% 0.59/0.76  ((a299) != (a293))
% 0.59/0.76  ((a325) != (a296))
% 0.59/0.76  ((a287) != (a334))
% 0.59/0.76  (-. (c2_1 (a293)))
% 0.59/0.76  ((a293) != (a335))
% 0.59/0.76  ((a343) != (a337))
% 0.59/0.76  ((a286) != (a347))
% 0.59/0.76  (zenon_X22 != (a333))
% 0.59/0.76  (zenon_X20 != (a301))
% 0.59/0.76  ((a343) != (a340))
% 0.59/0.76  ((a287) != (a288))
% 0.59/0.76  ((a343) != (a333))
% 0.59/0.76  ((a333) != (a306))
% 0.59/0.76  ((a345) != (a333))
% 0.59/0.76  ((a316) != (a307))
% 0.59/0.76  ((a344) != zenon_X22)
% 0.59/0.76  ((a297) != (a347))
% 0.59/0.76  ((a343) != (a286))
% 0.59/0.76  ((a301) != (a283))
% 0.59/0.76  ((a297) != (a286))
% 0.59/0.76  ((a285) != (a283))
% 0.59/0.76  ((a303) != (a347))
% 0.59/0.76  ((a340) != (a326))
% 0.59/0.76  ((a291) != (a318))
% 0.59/0.76  ((a311) != (a298))
% 0.59/0.76  ((a302) != (a294))
% 0.59/0.76  ((a282) != (a347))
% 0.59/0.76  ((a296) != (a286))
% 0.59/0.76  ((a302) != (a307))
% 0.59/0.76  ((a302) != (a336))
% 0.59/0.76  ((a302) != (a335))
% 0.59/0.76  ((a287) != (a326))
% 0.59/0.76  ((a334) != (a310))
% 0.59/0.76  ((a309) != (a335))
% 0.59/0.76  (-. (c2_1 (a324)))
% 0.59/0.76  ((a315) != (a291))
% 0.59/0.76  ((a287) != (a345))
% 0.59/0.76  (zenon_X10 != (a322))
% 0.59/0.76  ((a307) != (a327))
% 0.59/0.76  ((a345) != (a335))
% 0.59/0.76  ((a305) != (a319))
% 0.59/0.76  (hskp31)
% 0.59/0.76  (zenon_X22 != (a319))
% 0.59/0.76  ((a301) != (a310))
% 0.59/0.76  ((a283) != (a324))
% 0.59/0.76  ((a284) != (a317))
% 0.59/0.76  ((a315) != (a330))
% 0.59/0.76  ((a286) != (a291))
% 0.59/0.76  ((a289) != (a345))
% 0.59/0.76  ((a334) != (a324))
% 0.59/0.76  ((a302) != (a324))
% 0.59/0.76  (-. (c3_1 (a318)))
% 0.59/0.76  (-. (c0_1 (a333)))
% 0.59/0.76  ((a309) != (a337))
% 0.59/0.76  ((a287) != (a325))
% 0.59/0.76  ((a335) != (a282))
% 0.59/0.76  (zenon_X0 != (a345))
% 0.59/0.76  ((a342) != (a317))
% 0.59/0.76  ((a300) != (a319))
% 0.59/0.76  ((a313) != (a336))
% 0.59/0.76  ((a327) != (a337))
% 0.59/0.76  ((a298) != (a335))
% 0.59/0.76  (c3_1 (a304))
% 0.59/0.76  ((a300) != (a347))
% 0.59/0.76  ((a330) != (a345))
% 0.59/0.76  (-. (c0_1 (a290)))
% 0.59/0.76  ((a325) != (a333))
% 0.59/0.76  ((a340) != (a310))
% 0.59/0.76  (zenon_X0 != (a290))
% 0.59/0.76  ((a298) != (a326))
% 0.59/0.76  ((a302) != (a337))
% 0.59/0.76  ((a316) != (a284))
% 0.59/0.76  ((a294) != (a326))
% 0.59/0.76  (c2_1 (a298))
% 0.59/0.76  ((a319) != (a283))
% 0.59/0.76  ((a331) != (a326))
% 0.59/0.76  ((a334) != (a291))
% 0.59/0.76  ((a303) != (a344))
% 0.59/0.76  ((a315) != zenon_X22)
% 0.59/0.76  ((a285) != (a347))
% 0.59/0.76  ((a297) != (a310))
% 0.59/0.76  ((a282) != (a309))
% 0.59/0.76  ((a299) != (a324))
% 0.59/0.76  ((a309) != (a336))
% 0.59/0.76  ((a304) != (a307))
% 0.59/0.76  ((a333) != (a336))
% 0.59/0.76  ((a287) != (a291))
% 0.59/0.76  ((a335) != (a310))
% 0.59/0.76  ((a336) != (a310))
% 0.59/0.76  ((a288) != zenon_X22)
% 0.59/0.76  ((a342) != (a335))
% 0.59/0.76  ((a330) != (a307))
% 0.59/0.76  (-. (c3_1 (a301)))
% 0.59/0.76  (-. (c1_1 (a327)))
% 0.59/0.76  ((a344) != (a331))
% 0.59/0.76  ((a340) != (a319))
% 0.59/0.76  ((a302) != (a298))
% 0.59/0.76  ((a336) != (a337))
% 0.59/0.76  ((a296) != (a282))
% 0.59/0.76  ((a282) != (a298))
% 0.59/0.76  ((a315) != (a334))
% 0.59/0.76  ((a293) != (a288))
% 0.59/0.76  ((a285) != (a291))
% 0.59/0.76  ((a282) != (a288))
% 0.59/0.76  ((a331) != (a288))
% 0.59/0.76  ((a345) != (a326))
% 0.59/0.76  ((a345) != (a294))
% 0.59/0.76  ((a315) != (a306))
% 0.59/0.76  ((a342) != (a347))
% 0.59/0.76  ((a298) != (a313))
% 0.59/0.76  ((a334) != (a319))
% 0.59/0.76  ((a330) != (a337))
% 0.59/0.76  ((a343) != (a297))
% 0.59/0.76  ((a307) != (a297))
% 0.59/0.76  ((a294) != (a312))
% 0.59/0.76  (-. (c3_1 (a299)))
% 0.59/0.76  ((a282) != zenon_X22)
% 0.59/0.76  ((a317) != (a296))
% 0.59/0.76  (-. (c0_1 (a327)))
% 0.59/0.76  ((a289) != (a294))
% 0.59/0.76  ((a304) != (a319))
% 0.59/0.76  ((a319) != (a306))
% 0.59/0.76  ((a315) != (a290))
% 0.59/0.76  (-. (c2_1 (a327)))
% 0.59/0.76  ((a284) != (a318))
% 0.59/0.76  ((a282) != (a324))
% 0.59/0.76  (zenon_X10 != (a305))
% 0.59/0.76  ((a287) != (a304))
% 0.59/0.76  ((a345) != (a347))
% 0.59/0.76  ((a336) != (a290))
% 0.59/0.76  ((a319) != (a288))
% 0.59/0.76  ((a298) != (a310))
% 0.59/0.76  ((a288) != (a316))
% 0.59/0.76  ((a313) != (a291))
% 0.59/0.76  ((a285) != (a337))
% 0.59/0.76  ((a315) != (a322))
% 0.59/0.76  (c1_1 (a345))
% 0.59/0.76  ((a331) != (a319))
% 0.59/0.76  (-. (c0_1 (a306)))
% 0.59/0.76  ((a333) != (a316))
% 0.59/0.76  ((a330) != (a333))
% 0.59/0.76  ((a327) != (a312))
% 0.59/0.76  ((a327) != (a333))
% 0.59/0.76  (-. (c0_1 (a317)))
% 0.59/0.76  (c2_1 (a287))
% 0.59/0.76  ((a287) != (a324))
% 0.59/0.76  (-. (c2_1 (a305)))
% 0.59/0.76  ((a293) != (a337))
% 0.59/0.76  ((a307) != (a344))
% 0.59/0.76  ((a301) != (a306))
% 0.59/0.76  ((a297) != (a319))
% 0.59/0.76  ((a287) != (a292))
% 0.59/0.76  ((a287) != (a307))
% 0.59/0.76  ((a285) != (a307))
% 0.59/0.76  (-. (c1_1 (a292)))
% 0.59/0.76  ((a294) != (a318))
% 0.59/0.76  ((a303) != (a309))
% 0.59/0.76  ((a330) != (a324))
% 0.59/0.76  ((a317) != (a286))
% 0.59/0.76  (hskp25)
% 0.59/0.76  (hskp49)
% 0.59/0.76  ((a317) != (a292))
% 0.59/0.76  ((a289) != (a334))
% 0.59/0.76  ((a311) != (a317))
% 0.59/0.76  (c0_1 (a309))
% 0.59/0.76  ((a317) != (a334))
% 0.59/0.76  ((a294) != (a305))
% 0.59/0.76  ((a303) != (a292))
% 0.59/0.76  ((a302) != (a282))
% 0.59/0.76  ((a294) != (a324))
% 0.59/0.76  ((a284) != (a283))
% 0.59/0.76  ((a334) != (a337))
% 0.59/0.76  ((a285) != (a282))
% 0.59/0.76  ((a303) != (a313))
% 0.59/0.76  ((a316) != (a310))
% 0.59/0.76  ((a340) != (a336))
% 0.59/0.76  (c0_1 (a299))
% 0.59/0.76  ((a322) != (a310))
% 0.59/0.76  ((a319) != (a326))
% 0.59/0.76  ((a285) != (a317))
% 0.59/0.76  ((a330) != (a327))
% 0.59/0.76  ((a344) != (a316))
% 0.59/0.76  ((a331) != (a286))
% 0.59/0.76  (c2_1 zenon_X10)
% 0.59/0.76  ((a299) != (a317))
% 0.59/0.76  ((a325) != (a324))
% 0.59/0.76  ((a296) != (a291))
% 0.59/0.76  (-. (c2_1 (a312)))
% 0.59/0.76  (zenon_X20 != (a345))
% 0.59/0.76  ((a315) != (a283))
% 0.59/0.76  ((a288) != (a318))
% 0.59/0.76  ((a303) != (a325))
% 0.59/0.76  ((a311) != (a284))
% 0.59/0.76  ((a282) != (a331))
% 0.59/0.76  (c2_1 (a296))
% 0.59/0.76  (-. (c3_1 (a286)))
% 0.59/0.76  ((a307) != (a333))
% 0.59/0.76  ((a284) != (a322))
% 0.59/0.76  ((a299) != (a327))
% 0.59/0.76  ((a345) != (a324))
% 0.59/0.76  ((a345) != (a318))
% 0.59/0.76  (-. (c2_1 (a335)))
% 0.59/0.76  ((a293) != (a307))
% 0.59/0.76  ((a331) != (a333))
% 0.59/0.76  (-. (c1_1 (a291)))
% 0.59/0.76  (c3_1 (a343))
% 0.59/0.76  ((a282) != (a306))
% 0.59/0.76  ((a289) != (a290))
% 0.59/0.76  ((a342) != (a283))
% 0.59/0.76  ((a302) != (a284))
% 0.59/0.76  ((a298) != (a288))
% 0.59/0.76  ((a311) != (a316))
% 0.59/0.76  ((a345) != (a311))
% 0.59/0.76  ((a291) != (a292))
% 0.59/0.76  ((a302) != (a300))
% 0.59/0.76  ((a316) != (a334))
% 0.59/0.76  (hskp4)
% 0.59/0.76  ((a284) != (a313))
% 0.59/0.76  ((a325) != (a337))
% 0.59/0.76  (zenon_X20 != zenon_X22)
% 0.59/0.76  ((a313) != (a292))
% 0.59/0.76  ((a287) != (a327))
% 0.59/0.76  ((a298) != (a293))
% 0.59/0.76  ((a304) != (a316))
% 0.59/0.76  ((a285) != (a294))
% 0.59/0.76  ((a307) != (a310))
% 0.59/0.76  ((a296) != (a342))
% 0.59/0.76  ((a304) != (a333))
% 0.59/0.76  ((a322) != (a333))
% 0.59/0.76  ((a340) != (a288))
% 0.59/0.76  ((a313) != (a344))
% 0.59/0.76  ((a316) != (a324))
% 0.59/0.76  ((a327) != (a310))
% 0.59/0.76  (-. (c0_1 (a345)))
% 0.59/0.76  ((a293) != (a306))
% 0.59/0.76  ((a289) != (a307))
% 0.59/0.76  (zenon_X20 != (a337))
% 0.59/0.76  ((a333) != (a290))
% 0.59/0.76  (c3_1 (a305))
% 0.59/0.76  ((a291) != (a312))
% 0.59/0.76  (-. (c1_1 (a310)))
% 0.59/0.76  ((a293) != (a336))
% 0.59/0.76  ((a326) != (a316))
% 0.59/0.76  (zenon_X0 != (a306))
% 0.59/0.76  ((a344) != (a330))
% 0.59/0.76  (zenon_X0 != (a337))
% 0.59/0.76  ((a288) != (a292))
% 0.59/0.76  ((a315) != (a326))
% 0.59/0.76  ((a342) != (a301))
% 0.59/0.76  ((a330) != (a301))
% 0.59/0.76  ((a343) != (a312))
% 0.59/0.76  ((a307) != (a312))
% 0.59/0.76  ((a325) != (a294))
% 0.59/0.76  ((a325) != (a347))
% 0.59/0.76  ((a305) != (a286))
% 0.59/0.76  (hskp28)
% 0.59/0.76  ((a322) != (a292))
% 0.59/0.76  ((a304) != (a282))
% 0.59/0.76  (c3_1 (a287))
% 0.59/0.76  ((a327) != (a334))
% 0.59/0.76  (hskp6)
% 0.59/0.76  (zenon_X20 != (a294))
% 0.59/0.76  ((a299) != (a336))
% 0.59/0.76  ((a307) != (a335))
% 0.59/0.76  (-. (c1_1 (a286)))
% 0.59/0.76  ((a343) != (a319))
% 0.59/0.76  (hskp0)
% 0.59/0.76  (hskp14)
% 0.59/0.76  ((a284) != (a294))
% 0.59/0.76  ((a309) != (a312))
% 0.59/0.76  ((a296) != (a318))
% 0.59/0.76  ((a286) != (a309))
% 0.59/0.76  ((a293) != (a316))
% 0.59/0.76  ((a293) != (a292))
% 0.59/0.76  ((a294) != (a300))
% 0.59/0.76  (c2_1 (a331))
% 0.59/0.76  ((a319) != (a292))
% 0.59/0.76  ((a331) != (a291))
% 0.59/0.76  ((a345) != (a309))
% 0.59/0.76  ((a343) != (a307))
% 0.59/0.76  ((a299) != (a301))
% 0.59/0.76  ((a330) != (a291))
% 0.59/0.76  ((a331) != (a283))
% 0.59/0.76  ((a344) != (a294))
% 0.59/0.76  ((a289) != (a305))
% 0.59/0.76  ((a315) != (a309))
% 0.59/0.76  (zenon_X22 != (a318))
% 0.59/0.76  ((a330) != (a290))
% 0.59/0.76  ((a296) != (a309))
% 0.59/0.76  (c3_1 (a293))
% 0.59/0.76  (c0_1 (a315))
% 0.59/0.76  (hskp10)
% 0.59/0.76  (c0_1 zenon_X0)
% 0.59/0.76  ((a316) != (a301))
% 0.59/0.76  ((a343) != (a282))
% 0.59/0.76  ((a313) != (a337))
% 0.59/0.76  ((a291) != (a317))
% 0.59/0.76  ((a286) != (a288))
% 0.59/0.76  ((a293) != (a318))
% 0.59/0.76  ((a303) != (a282))
% 0.59/0.76  ((a285) != (a305))
% 0.59/0.76  ((a315) != (a331))
% 0.59/0.76  ((a340) != (a282))
% 0.59/0.76  ((a291) != (a316))
% 0.59/0.76  (zenon_X0 != (a307))
% 0.59/0.76  (c2_1 (a297))
% 0.59/0.76  ((a307) != (a319))
% 0.59/0.76  (-. (c2_1 (a347)))
% 0.59/0.76  ((a293) != (a284))
% 0.59/0.76  ((a296) != (a324))
% 0.59/0.76  ((a305) != (a337))
% 0.59/0.76  ((a317) != (a337))
% 0.59/0.76  ((a309) != (a291))
% 0.59/0.76  (zenon_X20 != (a340))
% 0.59/0.76  ((a289) != (a318))
% 0.59/0.76  ((a343) != (a301))
% 0.59/0.76  (zenon_X10 != (a319))
% 0.59/0.76  ((a296) != (a283))
% 0.59/0.76  ((a316) != (a312))
% 0.59/0.76  ((a284) != (a291))
% 0.59/0.76  (-. (c3_1 (a307)))
% 0.59/0.76  ((a319) != (a347))
% 0.59/0.76  ((a335) != (a311))
% 0.59/0.76  ((a305) != (a310))
% 0.59/0.76  ((a302) != (a318))
% 0.59/0.76  ((a296) != (a304))
% 0.59/0.76  ((a325) != (a300))
% 0.59/0.76  ((a307) != (a336))
% 0.59/0.76  (zenon_X10 != (a291))
% 0.59/0.76  ((a299) != (a345))
% 0.59/0.76  ((a343) != (a284))
% 0.59/0.76  (zenon_X20 != (a307))
% 0.59/0.76  ((a334) != (a333))
% 0.59/0.76  ((a330) != (a286))
% 0.59/0.76  (zenon_X20 != (a290))
% 0.59/0.76  ((a285) != (a322))
% 0.59/0.76  ((a343) != (a306))
% 0.59/0.76  ((a300) != (a292))
% 0.59/0.76  ((a287) != (a322))
% 0.59/0.76  ((a333) != (a342))
% 0.59/0.76  (-. (c3_1 (a334)))
% 0.59/0.76  (zenon_X20 != (a331))
% 0.59/0.76  ((a284) != (a300))
% 0.59/0.76  ((a301) != (a286))
% 0.59/0.76  ((a289) != (a327))
% 0.59/0.76  ((a343) != (a283))
% 0.59/0.76  (c1_1 (a317))
% 0.59/0.76  ((a315) != (a296))
% 0.59/0.76  (-. (c0_1 (a324)))
% 0.59/0.76  (-. (c3_1 (a284)))
% 0.59/0.76  ((a315) != (a345))
% 0.59/0.76  ((a305) != zenon_X22)
% 0.59/0.76  ((a304) != (a300))
% 0.59/0.76  ((a300) != (a337))
% 0.59/0.76  ((a302) != (a322))
% 0.59/0.76  ((a302) != (a327))
% 0.59/0.76  ((a317) != (a331))
% 0.59/0.76  (-. (c1_1 (a282)))
% 0.59/0.76  ((a315) != (a293))
% 0.59/0.76  (hskp52)
% 0.59/0.76  ((a297) != (a317))
% 0.59/0.76  ((a309) != (a288))
% 0.59/0.76  ((a311) != (a319))
% 0.59/0.76  ((a315) != (a319))
% 0.59/0.76  (c3_1 (a326))
% 0.59/0.76  ((a311) != (a290))
% 0.59/0.76  (hskp48)
% 0.59/0.76  (c2_1 (a285))
% 0.59/0.76  ((a334) != (a305))
% 0.59/0.76  ((a309) != (a347))
% 0.59/0.76  (zenon_X20 != (a299))
% 0.59/0.76  ((a304) != (a327))
% 0.59/0.76  ((a315) != (a307))
% 0.59/0.76  (-. (c1_1 (a342)))
% 0.59/0.76  (hskp38)
% 0.59/0.76  *)
% 0.59/0.76  (* NO-PROOF *)
% 0.59/0.76  % SZS status GaveUp
% 0.59/0.76  Number of rewrites on terms: 0
% 0.59/0.76  Number of rewrites on props: 0
% 0.59/0.76  nodes searched: 10130
% 0.59/0.76  max branch formulas: 1707
% 0.59/0.76  proof nodes created: 611
% 0.59/0.76  formulas created: 30060
% 0.59/0.76  
%------------------------------------------------------------------------------