↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n011.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:03:19 EDT 2024

% Result   : Unknown 0.21s 0.58s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13  % Problem  : NLP099-1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.13  % Command  : run_zenon_modulo %d %s
% 0.13/0.35  % Computer : n011.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit : 300
% 0.13/0.35  % WCLimit  : 300
% 0.13/0.35  % DateTime : Sat Jun 22 22:35:54 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 0.21/0.58  Zenon error: exhausted search space without finding a proof
% 0.21/0.58  (* Current branch:
% 0.21/0.58  ((skf12 zenon_X52) != zenon_X105)
% 0.21/0.58  ((skf26 zenon_X0 zenon_X2) != zenon_X120)
% 0.21/0.58  (see (skc16) (skf20 zenon_X23))
% 0.21/0.58  ((skc6) != zenon_X91)
% 0.21/0.58  (-. (nonreflexive (skc16) (skf21 zenon_X9)))
% 0.21/0.58  ((skf21 zenon_X15) != zenon_X149)
% 0.21/0.58  ((skc18) != zenon_X153)
% 0.21/0.58  (customer zenon_X3 (skf30 zenon_X3 zenon_X5))
% 0.21/0.58  (-. (event (skc16) zenon_X105))
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X157)
% 0.21/0.58  ((skf12 zenon_X61) != zenon_X161)
% 0.21/0.58  ((skc18) != zenon_X165)
% 0.21/0.58  (agent (skc16) (skf20 zenon_X26) zenon_X26)
% 0.21/0.58  ((skf11 zenon_X49) != zenon_X101)
% 0.21/0.58  (human_person (skc5) (skf13 zenon_X64))
% 0.21/0.58  (nonreflexive (skc5) (skf12 zenon_X58))
% 0.21/0.58  ((skf21 zenon_X9) != zenon_X208)
% 0.21/0.58  ((skf26 zenon_X0 zenon_X2) != zenon_X109)
% 0.21/0.58  (in zenon_X65 (skf17 zenon_X65 zenon_X67 zenon_X68) zenon_X67)
% 0.21/0.58  (-. (restaurant (skc5) zenon_X189))
% 0.21/0.58  (restaurant (skc16) (skc18))
% 0.21/0.58  (-. (human_person (skc16) zenon_X175))
% 0.21/0.58  (-. (restaurant (skc16) zenon_X176))
% 0.21/0.58  ((skf12 zenon_X61) != zenon_X123)
% 0.21/0.58  (-. (drink (skc16) zenon_X123))
% 0.21/0.58  (actual_world (skc16))
% 0.21/0.58  ((skc16) != zenon_X85)
% 0.21/0.58  (-. (restaurant (skc5) zenon_X143))
% 0.21/0.58  (-. (event (skc5) zenon_X139))
% 0.21/0.58  (past (skc5) (skf11 zenon_X46))
% 0.21/0.58  (zenon_X11 != zenon_X9)
% 0.21/0.58  (patient (skc5) (skf12 zenon_X73) (skc6))
% 0.21/0.58  ((skc17) != zenon_X91)
% 0.21/0.58  (past (skc16) (skf20 zenon_X19))
% 0.21/0.58  ((skc18) != zenon_X205)
% 0.21/0.58  ((skf12 zenon_X52) != zenon_X149)
% 0.21/0.58  ((skf13 zenon_X64) != zenon_X180)
% 0.21/0.58  (actual_world (skc5))
% 0.21/0.58  (-. (restaurant (skc5) zenon_X165))
% 0.21/0.58  ((skf21 zenon_X9) != zenon_X118)
% 0.21/0.58  (human_person (skc16) (skf22 zenon_X7))
% 0.21/0.58  (-. (restaurant (skc5) zenon_X146))
% 0.21/0.58  ((skf13 zenon_X64) != zenon_X175)
% 0.21/0.58  (-. (human_person (skc16) zenon_X124))
% 0.21/0.58  ((skf13 zenon_X64) != zenon_X119)
% 0.21/0.58  (-. (drink (skc16) zenon_X208))
% 0.21/0.58  (agent (skc5) (skf11 zenon_X70) zenon_X70)
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X203)
% 0.21/0.58  (customer zenon_X33 (skf17 zenon_X33 zenon_X36 zenon_X37))
% 0.21/0.58  (in zenon_X27 (skf30 zenon_X27 zenon_X28) (skf26 zenon_X27 zenon_X28))
% 0.21/0.58  ((skf21 zenon_X9) != (skf12 zenon_X61))
% 0.21/0.58  (drink (skc5) (skf12 zenon_X61))
% 0.21/0.58  ((skf20 zenon_X17) != zenon_X101)
% 0.21/0.58  ((skc18) != zenon_X109)
% 0.21/0.58  (coffee (skc16) (skc17))
% 0.21/0.58  (-. (restaurant (skc16) (skf26 zenon_X0 zenon_X2)))
% 0.21/0.58  (-. (coffee (skc16) zenon_X96))
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X125)
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X126)
% 0.21/0.58  (-. (event (skc16) zenon_X149))
% 0.21/0.58  (-. (human_person (skc16) zenon_X157))
% 0.21/0.58  ((skf21 zenon_X9) != zenon_X161)
% 0.21/0.58  ((skc18) != zenon_X115)
% 0.21/0.58  (-. (human_person (skc16) zenon_X119))
% 0.21/0.58  (-. (restaurant (skc5) (skf26 zenon_X0 zenon_X2)))
% 0.21/0.58  ((skf13 zenon_X64) != zenon_X124)
% 0.21/0.58  (-. (restaurant (skc5) zenon_X112))
% 0.21/0.58  ((skf13 zenon_X64) != zenon_X125)
% 0.21/0.58  (-. (drink (skc16) zenon_X202))
% 0.21/0.58  (nonreflexive (skc16) (skf20 zenon_X21))
% 0.21/0.58  ((skf21 zenon_X15) != zenon_X139)
% 0.21/0.58  (ssSkC0)
% 0.21/0.58  ((skf12 zenon_X61) != zenon_X174)
% 0.21/0.58  ((skc5) != zenon_X85)
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X209)
% 0.21/0.58  ((skf20 zenon_X21) != (skf21 zenon_X9))
% 0.21/0.58  (see (skc5) (skf11 zenon_X40))
% 0.21/0.58  ((skf21 zenon_X9) != zenon_X156)
% 0.21/0.58  (-. (drink (skc16) zenon_X179))
% 0.21/0.58  ((skf21 zenon_X15) != zenon_X105)
% 0.21/0.58  ((skf11 zenon_X49) != zenon_X105)
% 0.21/0.58  (event (skc5) (skf11 zenon_X49))
% 0.21/0.58  ((skf26 zenon_X0 zenon_X2) != zenon_X115)
% 0.21/0.58  (-. (human_person (skc16) zenon_X126))
% 0.21/0.58  (-. (drink (skc16) zenon_X161))
% 0.21/0.58  (zenon_X0 != (skc5))
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X187)
% 0.21/0.58  (nonreflexive (skc5) (skf11 zenon_X43))
% 0.21/0.58  (-. (restaurant (skc16) zenon_X199))
% 0.21/0.58  (-. (restaurant (skc16) zenon_X115))
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X180)
% 0.21/0.58  (restaurant zenon_X0 (skf26 zenon_X0 zenon_X2))
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X124)
% 0.21/0.58  ((skc18) != zenon_X176)
% 0.21/0.58  ((skc18) != zenon_X168)
% 0.21/0.58  ((skc17) != zenon_X96)
% 0.21/0.58  (-. (restaurant (skc16) zenon_X158))
% 0.21/0.58  (-. (drink (skc16) (skf12 zenon_X61)))
% 0.21/0.58  (past (skc16) (skf21 zenon_X13))
% 0.21/0.58  (-. (restaurant (skc5) zenon_X192))
% 0.21/0.58  (drink (skc16) (skf21 zenon_X9))
% 0.21/0.58  ((skf20 zenon_X17) != zenon_X105)
% 0.21/0.58  ((skf13 zenon_X64) != zenon_X126)
% 0.21/0.58  (-. (restaurant (skc5) zenon_X168))
% 0.21/0.58  (past (skc5) (skf12 zenon_X55))
% 0.21/0.58  (event (skc16) (skf21 zenon_X15))
% 0.21/0.58  (nonreflexive (skc16) (skf21 zenon_X11))
% 0.21/0.58  (-. (drink (skc16) zenon_X118))
% 0.21/0.58  ((skf21 zenon_X9) != zenon_X179)
% 0.21/0.58  ((skf12 zenon_X61) != zenon_X179)
% 0.21/0.58  ((skf21 zenon_X9) != zenon_X123)
% 0.21/0.58  (-. (restaurant (skc16) zenon_X171))
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X162)
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X119)
% 0.21/0.58  ((skc16) != (skc5))
% 0.21/0.58  (patient (skc16) (skf21 zenon_X25) (skc17))
% 0.21/0.58  (zenon_X0 != (skc16))
% 0.21/0.58  ((skf22 zenon_X7) != zenon_X175)
% 0.21/0.58  (-. (human_person (skc16) zenon_X180))
% 0.21/0.58  ((skf20 zenon_X17) != zenon_X139)
% 0.21/0.58  ((skc18) != zenon_X120)
% 0.21/0.58  ((skc18) != zenon_X171)
% 0.21/0.58  (-. (drink (skc16) zenon_X156))
% 0.21/0.58  (-. (restaurant (skc16) zenon_X153))
% 0.21/0.58  ((skc18) != zenon_X143)
% 0.21/0.58  ((skc18) != zenon_X199)
% 0.21/0.58  ((skf11 zenon_X49) != zenon_X139)
% 0.21/0.58  ((skf13 zenon_X64) != zenon_X157)
% 0.21/0.58  (-. (human_person (skc16) zenon_X162))
% 0.21/0.58  ((skc18) != zenon_X158)
% 0.21/0.58  ((skf13 zenon_X64) != zenon_X162)
% 0.21/0.58  (-. (restaurant (skc5) zenon_X109))
% 0.21/0.58  (-. (drink (skc16) zenon_X174))
% 0.21/0.58  (-. (human_person (skc16) zenon_X209))
% 0.21/0.58  ((skf21 zenon_X11) != (skf21 zenon_X9))
% 0.21/0.58  ((skf12 zenon_X52) != zenon_X139)
% 0.21/0.58  ((skf12 zenon_X52) != zenon_X101)
% 0.21/0.58  (-. (restaurant (skc5) (skc18)))
% 0.21/0.58  (agent (skc16) (skf21 zenon_X30) (skf22 zenon_X30))
% 0.21/0.58  ((skf12 zenon_X58) != (skf21 zenon_X9))
% 0.21/0.58  ((skf21 zenon_X15) != zenon_X101)
% 0.21/0.58  (patient (skc5) (skf11 zenon_X79) (skf13 zenon_X79))
% 0.21/0.58  (-. (human_person (skc16) zenon_X187))
% 0.21/0.58  ((skc18) != zenon_X146)
% 0.21/0.58  (-. (human_person (skc16) zenon_X203))
% 0.21/0.58  (-. (restaurant (skc16) zenon_X205))
% 0.21/0.58  ((skf11 zenon_X43) != (skf21 zenon_X9))
% 0.21/0.58  ((skc18) != zenon_X112)
% 0.21/0.58  (coffee (skc5) (skc6))
% 0.21/0.58  ((skf11 zenon_X49) != zenon_X149)
% 0.21/0.58  (-. (human_person (skc16) zenon_X125))
% 0.21/0.58  ((skf12 zenon_X61) != zenon_X156)
% 0.21/0.58  (-. (restaurant (skc16) zenon_X120))
% 0.21/0.58  ((skc18) != (skf26 zenon_X0 zenon_X2))
% 0.21/0.58  ((skc6) != zenon_X96)
% 0.21/0.58  ((skf20 zenon_X17) != zenon_X149)
% 0.21/0.58  ((skf21 zenon_X9) != zenon_X202)
% 0.21/0.58  (-. (coffee (skc5) zenon_X91))
% 0.21/0.58  ((skf12 zenon_X61) != zenon_X118)
% 0.21/0.58  (-. (actual_world zenon_X85))
% 0.21/0.58  ((skf21 zenon_X9) != zenon_X174)
% 0.21/0.58  (-. (event (skc5) zenon_X101))
% 0.21/0.58  (event (skc16) (skf20 zenon_X17))
% 0.21/0.58  (patient (skc16) (skf20 zenon_X32) (skf22 zenon_X32))
% 0.21/0.58  (event (skc5) (skf12 zenon_X52))
% 0.21/0.58  ((skf26 zenon_X0 zenon_X2) != zenon_X112)
% 0.21/0.58  (agent (skc5) (skf12 zenon_X76) (skf13 zenon_X76))
% 0.21/0.58  *)
% 0.21/0.58  (* NO-PROOF *)
% 0.21/0.58  % SZS status GaveUp
% 0.21/0.58  Number of rewrites on terms: 0
% 0.21/0.58  Number of rewrites on props: 0
% 0.21/0.58  nodes searched: 706
% 0.21/0.58  max branch formulas: 499
% 0.21/0.58  proof nodes created: 114
% 0.21/0.58  formulas created: 7051
% 0.21/0.58  
%------------------------------------------------------------------------------