↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n015.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:52 EDT 2024

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

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12  % Problem  : SYN526-1 : TPTP v8.2.0. Released v2.1.0.
% 0.04/0.12  % Command  : run_zenon_modulo %d %s
% 0.12/0.34  % Computer : n015.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Mon Jun 24 01:19:09 EDT 2024
% 0.12/0.34  % CPUTime  : 
% 0.42/0.59  Zenon error: exhausted search space without finding a proof
% 0.42/0.59  (* Current branch:
% 0.42/0.59  ((a240) != zenon_X10)
% 0.42/0.59  ((a225) != zenon_X8)
% 0.42/0.59  (c1_2 zenon_X1 (a235))
% 0.42/0.59  (zenon_X40 != zenon_X3)
% 0.42/0.59  ((a230) != zenon_X10)
% 0.42/0.59  (zenon_X39 != zenon_X3)
% 0.42/0.59  (c1_2 zenon_X53 (a228))
% 0.42/0.59  (c5_1 (a240))
% 0.42/0.59  (zenon_X39 != zenon_X1)
% 0.42/0.59  (c5_2 (a237) (a244))
% 0.42/0.59  (ssSkP0 zenon_X8)
% 0.42/0.59  (zenon_X4 != zenon_X3)
% 0.42/0.59  (-. (c5_2 zenon_X3 (a235)))
% 0.42/0.59  (ssSkP0 zenon_X3)
% 0.42/0.59  (c4_1 zenon_X79)
% 0.42/0.59  (c5_1 zenon_X88)
% 0.42/0.59  (c4_2 (a230) (a244))
% 0.42/0.59  ((a240) != zenon_X14)
% 0.42/0.59  (ssSkC5)
% 0.42/0.59  (-. (c2_2 zenon_X0 (a228)))
% 0.42/0.59  (-. (ndr1_1 zenon_X29))
% 0.42/0.59  (zenon_X39 != zenon_X2)
% 0.42/0.59  ((a230) != zenon_X14)
% 0.42/0.59  ((a226) != (a241))
% 0.42/0.59  (ssSkP0 zenon_X16)
% 0.42/0.59  (zenon_X14 != zenon_X0)
% 0.42/0.59  (c1_2 zenon_X3 (a228))
% 0.42/0.59  ((a220) != zenon_X139)
% 0.42/0.59  ((a230) != zenon_X39)
% 0.42/0.59  (c1_1 zenon_X70)
% 0.42/0.59  (zenon_X16 != zenon_X3)
% 0.42/0.59  (ssSkP0 zenon_X1)
% 0.42/0.59  (c2_2 zenon_X0 (a220))
% 0.42/0.59  (zenon_X8 != zenon_X53)
% 0.42/0.59  ((a237) != zenon_X1)
% 0.42/0.59  (zenon_X16 != zenon_X2)
% 0.42/0.59  (c5_1 (a225))
% 0.42/0.59  ((a230) != zenon_X53)
% 0.42/0.59  ((a240) != zenon_X8)
% 0.42/0.59  (c4_1 zenon_X19)
% 0.42/0.59  (zenon_X29 != zenon_X0)
% 0.42/0.59  (c1_2 zenon_X1 (a228))
% 0.42/0.59  (c4_1 zenon_X73)
% 0.42/0.59  (c2_1 (a230))
% 0.42/0.59  ((a225) != zenon_X88)
% 0.42/0.59  (c1_2 zenon_X53 (a227))
% 0.42/0.59  ((a240) != zenon_X16)
% 0.42/0.59  (zenon_X40 != zenon_X0)
% 0.42/0.59  (-. (ndr1_1 zenon_X14))
% 0.42/0.59  ((a225) != zenon_X1)
% 0.42/0.59  (zenon_X14 != zenon_X3)
% 0.42/0.59  (zenon_X4 != zenon_X2)
% 0.42/0.59  (zenon_X10 != zenon_X0)
% 0.42/0.59  (zenon_X1 != zenon_X53)
% 0.42/0.59  (c5_1 zenon_X39)
% 0.42/0.59  (ssSkC3)
% 0.42/0.59  (c4_1 zenon_X13)
% 0.42/0.59  ((a230) != zenon_X7)
% 0.42/0.59  ((a220) != (a241))
% 0.42/0.59  (zenon_X10 != zenon_X2)
% 0.42/0.59  ((a244) != (a241))
% 0.42/0.59  ((a235) != zenon_X129)
% 0.42/0.59  (-. (c1_2 (a240) (a241)))
% 0.42/0.59  (zenon_X0 != zenon_X53)
% 0.42/0.59  (ssSkC4)
% 0.42/0.59  (zenon_X88 != zenon_X1)
% 0.42/0.59  (-. (c2_1 (a240)))
% 0.42/0.59  (-. (ssSkC1))
% 0.42/0.59  (c1_2 zenon_X3 (a235))
% 0.42/0.59  (c2_2 zenon_X53 (a220))
% 0.42/0.59  (c3_0)
% 0.42/0.59  (-. (c5_2 zenon_X0 (a228)))
% 0.42/0.59  (c2_1 (a237))
% 0.42/0.59  (zenon_X14 != zenon_X1)
% 0.42/0.59  (c4_2 zenon_X53 (a235))
% 0.42/0.59  (zenon_X29 != zenon_X1)
% 0.42/0.59  (ndr1_1 zenon_X1)
% 0.42/0.59  (c5_1 zenon_X4)
% 0.42/0.59  ((a228) != zenon_X157)
% 0.42/0.59  (zenon_X39 != zenon_X53)
% 0.42/0.59  ((a244) != zenon_X93)
% 0.42/0.59  (zenon_X4 != zenon_X53)
% 0.42/0.59  ((a230) != (a247))
% 0.42/0.59  (c2_2 zenon_X3 (a220))
% 0.42/0.59  (c4_2 zenon_X1 (a235))
% 0.42/0.59  (-. (c2_2 zenon_X2 (a228)))
% 0.42/0.59  (zenon_X10 != zenon_X3)
% 0.42/0.59  (zenon_X14 != zenon_X53)
% 0.42/0.59  (c1_2 zenon_X0 (a235))
% 0.42/0.59  ((a235) != zenon_X148)
% 0.42/0.59  (-. (c5_1 zenon_X1))
% 0.42/0.59  (zenon_X88 != zenon_X0)
% 0.42/0.59  (-. (c2_1 zenon_X2))
% 0.42/0.59  (-. (c5_1 zenon_X3))
% 0.42/0.59  ((a240) != zenon_X40)
% 0.42/0.59  (-. (c2_1 zenon_X53))
% 0.42/0.59  (ssSkP0 zenon_X2)
% 0.42/0.59  (-. (c1_0))
% 0.42/0.59  (c4_1 (a225))
% 0.42/0.59  ((a225) != zenon_X10)
% 0.42/0.59  (zenon_X7 != zenon_X1)
% 0.42/0.59  (c4_1 zenon_X6)
% 0.42/0.59  ((a228) != zenon_X114)
% 0.42/0.59  (ssSkP0 zenon_X0)
% 0.42/0.59  ((a230) != zenon_X8)
% 0.42/0.59  ((a230) != zenon_X88)
% 0.42/0.59  (ssSkP0 zenon_X14)
% 0.42/0.59  (ssSkC0)
% 0.42/0.59  ((a220) != zenon_X114)
% 0.42/0.59  (-. (ndr1_1 zenon_X88))
% 0.42/0.59  (zenon_X40 != zenon_X1)
% 0.42/0.59  ((a237) != zenon_X3)
% 0.42/0.59  ((a240) != zenon_X7)
% 0.42/0.59  (c1_2 (a225) (a226))
% 0.42/0.59  ((a225) != zenon_X3)
% 0.42/0.59  (c2_2 zenon_X51 (a244))
% 0.42/0.59  (-. (c5_2 zenon_X1 (a228)))
% 0.42/0.59  (-. (c5_2 (a240) (a241)))
% 0.42/0.59  ((a225) != zenon_X53)
% 0.42/0.59  ((a240) != zenon_X29)
% 0.42/0.59  (c5_1 zenon_X40)
% 0.42/0.59  (ssSkP0 (a240))
% 0.42/0.59  (-. (c3_1 (a247)))
% 0.42/0.59  (c1_1 zenon_X65)
% 0.42/0.59  ((a230) != zenon_X16)
% 0.42/0.59  ((a237) != zenon_X0)
% 0.42/0.59  (zenon_X4 != zenon_X0)
% 0.42/0.59  (c4_2 zenon_X53 (a227))
% 0.42/0.59  (ssSkP0 (a237))
% 0.42/0.59  (c4_2 (a225) (a244))
% 0.42/0.59  (c5_2 zenon_X49 (a244))
% 0.42/0.59  (zenon_X8 != zenon_X2)
% 0.42/0.59  ((a237) != zenon_X53)
% 0.42/0.59  (-. (c5_2 (a230) zenon_X94))
% 0.42/0.59  ((a225) != zenon_X39)
% 0.42/0.59  ((a230) != zenon_X4)
% 0.42/0.59  ((a225) != zenon_X40)
% 0.42/0.59  (c4_2 zenon_X86 (a220))
% 0.42/0.59  (-. (c1_2 zenon_X3 zenon_X139))
% 0.42/0.59  ((a244) != zenon_X47)
% 0.42/0.59  (c1_1 zenon_X57)
% 0.42/0.59  (zenon_X88 != zenon_X53)
% 0.42/0.59  (zenon_X39 != zenon_X0)
% 0.42/0.59  (-. (ndr1_1 zenon_X4))
% 0.42/0.59  (ndr1_1 (a240))
% 0.42/0.59  (zenon_X16 != zenon_X53)
% 0.42/0.59  (-. (c5_2 zenon_X2 (a235)))
% 0.42/0.59  (ssSkC8)
% 0.42/0.59  (c4_2 (a237) (a244))
% 0.42/0.59  ((a235) != zenon_X157)
% 0.42/0.59  (-. (c2_2 zenon_X1 (a228)))
% 0.42/0.59  (-. (c2_2 (a237) zenon_X47))
% 0.42/0.59  ((a240) != zenon_X3)
% 0.42/0.59  (-. (c2_1 zenon_X0))
% 0.42/0.59  (-. (ndr1_1 zenon_X10))
% 0.42/0.59  (c1_1 zenon_X62)
% 0.42/0.59  (zenon_X10 != zenon_X1)
% 0.42/0.59  (zenon_X88 != zenon_X3)
% 0.42/0.59  (-. (c1_2 zenon_X1 zenon_X129))
% 0.42/0.59  (c5_1 zenon_X7)
% 0.42/0.59  ((a230) != zenon_X2)
% 0.42/0.59  ((a225) != zenon_X0)
% 0.42/0.59  (-. (ndr1_1 zenon_X39))
% 0.42/0.59  (-. (c2_1 zenon_X1))
% 0.42/0.59  (ndr1_1 (a225))
% 0.42/0.59  (ndr1_1 zenon_X2)
% 0.42/0.59  (ssSkP0 zenon_X7)
% 0.42/0.59  (zenon_X7 != zenon_X3)
% 0.42/0.59  (-. (c5_2 zenon_X1 (a235)))
% 0.42/0.59  ((a228) != zenon_X129)
% 0.42/0.59  (ssSkP0 (a225))
% 0.42/0.59  ((a225) != zenon_X14)
% 0.42/0.59  ((a240) != zenon_X1)
% 0.42/0.59  (c2_2 zenon_X53 (a228))
% 0.42/0.59  (ssSkP0 zenon_X40)
% 0.42/0.59  ((a240) != zenon_X2)
% 0.42/0.59  ((a235) != zenon_X139)
% 0.42/0.59  (-. (c5_2 (a225) zenon_X95))
% 0.42/0.59  ((a244) != (a227))
% 0.42/0.59  (-. (c5_2 zenon_X2 (a228)))
% 0.42/0.59  (ssSkP0 (a230))
% 0.42/0.59  (zenon_X3 != zenon_X53)
% 0.42/0.59  ((a244) != zenon_X95)
% 0.42/0.59  (-. (c5_2 (a237) zenon_X110))
% 0.42/0.59  (zenon_X88 != zenon_X2)
% 0.42/0.59  ((a225) != zenon_X7)
% 0.42/0.59  ((a230) != (a240))
% 0.42/0.59  (c4_2 (a240) (a244))
% 0.42/0.59  ((a240) != zenon_X4)
% 0.42/0.59  (ndr1_1 (a230))
% 0.42/0.59  (c3_1 (a230))
% 0.42/0.59  (c4_1 zenon_X76)
% 0.42/0.59  ((a220) != zenon_X129)
% 0.42/0.59  ((a237) != zenon_X2)
% 0.42/0.59  ((a244) != (a235))
% 0.42/0.59  (-. (c5_1 zenon_X53))
% 0.42/0.59  (ndr1_0)
% 0.42/0.59  (-. (ssSkP0 zenon_X53))
% 0.42/0.59  ((a230) != zenon_X3)
% 0.42/0.59  (c1_2 zenon_X2 (a228))
% 0.42/0.59  (c2_2 zenon_X2 (a220))
% 0.42/0.59  ((a240) != zenon_X53)
% 0.42/0.59  (-. (c5_2 zenon_X3 (a228)))
% 0.42/0.59  ((a225) != zenon_X29)
% 0.42/0.59  (-. (c1_2 zenon_X53 zenon_X114))
% 0.42/0.59  (ndr1_1 zenon_X53)
% 0.42/0.59  (-. (c2_0))
% 0.42/0.59  ((a240) != zenon_X39)
% 0.42/0.59  (ssSkP0 zenon_X10)
% 0.42/0.59  (-. (ndr1_1 zenon_X7))
% 0.42/0.59  (zenon_X8 != zenon_X1)
% 0.42/0.59  (ssSkP0 zenon_X39)
% 0.42/0.59  (c5_1 zenon_X16)
% 0.42/0.59  ((a235) != zenon_X114)
% 0.42/0.59  ((a220) != zenon_X157)
% 0.42/0.59  ((a227) != zenon_X114)
% 0.42/0.59  (zenon_X2 != zenon_X53)
% 0.42/0.59  (c2_2 zenon_X1 (a220))
% 0.42/0.59  ((a230) != zenon_X1)
% 0.42/0.59  (-. (c1_2 zenon_X2 zenon_X148))
% 0.42/0.59  (c1_2 zenon_X82 (a220))
% 0.42/0.59  (-. (c5_2 zenon_X53 (a227)))
% 0.42/0.59  (zenon_X8 != zenon_X3)
% 0.42/0.59  (zenon_X7 != zenon_X0)
% 0.42/0.59  ((a244) != zenon_X110)
% 0.42/0.59  ((a220) != zenon_X148)
% 0.42/0.59  (c5_1 zenon_X10)
% 0.42/0.59  ((a225) != zenon_X2)
% 0.42/0.59  (-. (c3_2 (a247) zenon_X32))
% 0.42/0.59  (c4_2 zenon_X0 (a235))
% 0.42/0.59  (zenon_X29 != zenon_X53)
% 0.42/0.59  (c1_2 zenon_X53 (a235))
% 0.42/0.59  (c5_0)
% 0.42/0.59  (c4_2 zenon_X2 (a235))
% 0.42/0.59  (ssSkC2)
% 0.42/0.59  (-. (ndr1_1 zenon_X40))
% 0.42/0.59  (c3_2 (a240) (a241))
% 0.42/0.59  (zenon_X16 != zenon_X1)
% 0.42/0.59  ((a237) != (a240))
% 0.42/0.59  (ssSkP0 zenon_X29)
% 0.42/0.59  ((a244) != zenon_X94)
% 0.42/0.59  (c1_2 zenon_X0 (a228))
% 0.42/0.59  ((a225) != zenon_X16)
% 0.42/0.59  (zenon_X7 != zenon_X53)
% 0.42/0.59  (zenon_X29 != zenon_X3)
% 0.42/0.59  (ndr1_1 zenon_X0)
% 0.42/0.59  ((a228) != zenon_X148)
% 0.42/0.59  (zenon_X16 != zenon_X0)
% 0.42/0.59  (-. (ndr1_1 zenon_X16))
% 0.42/0.59  (zenon_X40 != zenon_X2)
% 0.42/0.59  (ssSkC6)
% 0.42/0.59  (c5_1 zenon_X14)
% 0.42/0.59  (zenon_X4 != zenon_X1)
% 0.42/0.59  (zenon_X14 != zenon_X2)
% 0.42/0.59  (-. (c5_2 (a237) zenon_X38))
% 0.42/0.59  (-. (c2_1 zenon_X3))
% 0.42/0.59  (-. (c5_2 zenon_X0 (a235)))
% 0.42/0.59  (-. (c2_2 zenon_X3 (a228)))
% 0.42/0.59  ((a240) != (a247))
% 0.42/0.59  (c5_1 zenon_X8)
% 0.42/0.59  (ssSkC7)
% 0.42/0.59  (-. (c5_1 zenon_X0))
% 0.42/0.59  ((a240) != zenon_X88)
% 0.42/0.59  (zenon_X40 != zenon_X53)
% 0.42/0.59  (c4_2 zenon_X3 (a235))
% 0.42/0.59  (zenon_X29 != zenon_X2)
% 0.42/0.59  (-. (c1_2 zenon_X0 zenon_X157))
% 0.42/0.59  (c5_1 (a230))
% 0.42/0.59  (c5_1 zenon_X29)
% 0.42/0.59  ((a244) != zenon_X38)
% 0.42/0.59  ((a240) != zenon_X0)
% 0.42/0.59  (ndr1_1 zenon_X3)
% 0.42/0.59  (zenon_X10 != zenon_X53)
% 0.42/0.59  ((a225) != zenon_X4)
% 0.42/0.59  (-. (c3_2 (a225) (a226)))
% 0.42/0.59  (c1_2 zenon_X2 (a235))
% 0.42/0.59  (-. (ndr1_1 zenon_X8))
% 0.42/0.59  (zenon_X8 != zenon_X0)
% 0.42/0.59  (ssSkP0 zenon_X88)
% 0.42/0.59  ((a228) != zenon_X139)
% 0.42/0.59  (ssSkP0 zenon_X4)
% 0.42/0.59  (c3_1 (a240))
% 0.42/0.59  ((a220) != (a228))
% 0.42/0.59  ((a244) != (a228))
% 0.42/0.59  (-. (c5_1 zenon_X2))
% 0.42/0.59  (-. (c5_2 zenon_X53 (a235)))
% 0.42/0.59  (ssSkC9)
% 0.42/0.59  ((a230) != zenon_X40)
% 0.42/0.59  ((a230) != zenon_X0)
% 0.42/0.59  (-. (c5_2 (a240) zenon_X93))
% 0.42/0.59  (zenon_X7 != zenon_X2)
% 0.42/0.59  ((a230) != zenon_X29)
% 0.42/0.59  *)
% 0.42/0.59  (* NO-PROOF *)
% 0.42/0.59  % SZS status GaveUp
% 0.42/0.59  Number of rewrites on terms: 0
% 0.42/0.59  Number of rewrites on props: 0
% 0.42/0.59  nodes searched: 1273
% 0.42/0.59  max branch formulas: 750
% 0.42/0.59  proof nodes created: 127
% 0.42/0.59  formulas created: 6952
% 0.42/0.59  
%------------------------------------------------------------------------------