↑ Up

ZenonModulo---0.5.0.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : LCL667+1.005 : TPTP v9.3.1. Released v4.0.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   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Mon Sep  7 01:34:22 PM UTC 2026

% Result   : Unknown 1.11s 1.44s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL667+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02  % Command  : run_zenon_modulo %d %s
% 0.08/0.38  % Computer : n005.cluster.edu
% 0.08/0.38  % Model    : x86_64 x86_64
% 0.08/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.38  % Memory   : 8046.5625MB
% 0.08/0.38  % OS       : Linux 6.8.0-71-generic
% 0.08/0.38  % CPULimit : 300
% 0.08/0.38  % WCLimit  : 300
% 0.08/0.38  % DateTime : Fri Sep  4 12:36:06 UTC 2026
% 0.08/0.38  % CPUTime  : 
% 1.11/1.44  Zenon error: exhausted search space without finding a proof
% 1.11/1.44  (* Current branch:
% 1.11/1.44  (zenon_Vca != zenon_Vba)
% 1.11/1.44  (zenon_Vaa != zenon_Vna)
% 1.11/1.44  (zenon_Vm != zenon_Vna)
% 1.11/1.44  (zenon_Vx != zenon_Vda)
% 1.11/1.44  (zenon_Vga != zenon_Vy)
% 1.11/1.44  (r1 zenon_X1 zenon_Vna)
% 1.11/1.44  (r1 zenon_X1 zenon_Vo)
% 1.11/1.44  (-. (p204 zenon_Vja))
% 1.11/1.44  (-. (p302 Tau_0))
% 1.11/1.44  (zenon_Vea != zenon_Vy)
% 1.11/1.44  (zenon_Vx != zenon_Vna)
% 1.11/1.44  (r1 zenon_X1 zenon_Vy)
% 1.11/1.44  (Tau_0 != zenon_X1)
% 1.11/1.44  (r1 zenon_X1 zenon_Vza)
% 1.11/1.44  (zenon_Vma != zenon_Vy)
% 1.11/1.44  (r1 Tau_0 zenon_Vv)
% 1.11/1.44  (-. (p205 zenon_Vea))
% 1.11/1.44  (zenon_Vr != zenon_Vfa)
% 1.11/1.44  (zenon_Vo != zenon_Vda)
% 1.11/1.44  (zenon_Vv != zenon_Vfa)
% 1.11/1.44  (zenon_Vgb != zenon_Vba)
% 1.11/1.44  (p601 Tau_0)
% 1.11/1.44  (-. (p305 zenon_Vo))
% 1.11/1.44  (zenon_Vya != zenon_Vba)
% 1.11/1.44  (zenon_Vs != zenon_Vfa)
% 1.11/1.44  (zenon_Vx != zenon_Vfa)
% 1.11/1.44  (-. (p402 zenon_X1))
% 1.11/1.44  (zenon_Vm != zenon_Vy)
% 1.11/1.44  (-. (p202 zenon_X1))
% 1.11/1.44  (zenon_Vv != zenon_Vna)
% 1.11/1.44  (zenon_Vaa != zenon_Vy)
% 1.11/1.44  (zenon_Vma != zenon_Vda)
% 1.11/1.44  (-. (p304 zenon_Vma))
% 1.11/1.44  (-. (p102 zenon_Vgb))
% 1.11/1.44  (-. (p205 zenon_Vv))
% 1.11/1.44  (zenon_Vo != zenon_Vna)
% 1.11/1.44  (zenon_Vm != zenon_Vja)
% 1.11/1.44  (r1 zenon_X1 zenon_Vfa)
% 1.11/1.44  (p404 zenon_X1)
% 1.11/1.44  (zenon_Vea != zenon_Vna)
% 1.11/1.44  (zenon_Vaa != zenon_Vja)
% 1.11/1.44  (zenon_Vcb != zenon_Vy)
% 1.11/1.44  (zenon_X9 != zenon_Vfa)
% 1.11/1.44  (-. (p504 zenon_X1))
% 1.11/1.44  (r1 zenon_X1 zenon_Vda)
% 1.11/1.44  (zenon_Vs != zenon_Vy)
% 1.11/1.44  (zenon_Vgb != zenon_Vfa)
% 1.11/1.44  (zenon_Vv != zenon_Vy)
% 1.11/1.44  (-. (p401 Tau_0))
% 1.11/1.44  (r1 zenon_X1 zenon_Voa)
% 1.11/1.44  (-. (p103 zenon_Veb))
% 1.11/1.44  (zenon_Vsa != zenon_Vba)
% 1.11/1.44  (-. (p104 zenon_Vsa))
% 1.11/1.44  (zenon_Vaa != zenon_Vda)
% 1.11/1.44  (r1 zenon_X1 zenon_Veb)
% 1.11/1.44  (zenon_Vo != zenon_Vfa)
% 1.11/1.44  (zenon_Vma != zenon_Vba)
% 1.11/1.44  (zenon_Vs != zenon_Vda)
% 1.11/1.44  (zenon_Vr != zenon_Vy)
% 1.11/1.44  (-. (p204 zenon_Vna))
% 1.11/1.44  (-. (p605 Tau_0))
% 1.11/1.44  (-. (p105 zenon_Vba))
% 1.11/1.44  (-. (p104 zenon_Vua))
% 1.11/1.44  (zenon_Vgb != zenon_Vda)
% 1.11/1.44  (-. (r1 Tau_0 zenon_Vna))
% 1.11/1.44  (-. (r1 Tau_0 zenon_Vja))
% 1.11/1.44  (-. (r1 Tau_0 zenon_Vfa))
% 1.11/1.44  (-. (r1 Tau_0 zenon_Vy))
% 1.11/1.44  (-. (r1 Tau_0 zenon_Vba))
% 1.11/1.44  (-. (r1 Tau_0 zenon_Vda))
% 1.11/1.44  (-. (p604 Tau_0))
% 1.11/1.44  (-. (p401 zenon_X1))
% 1.11/1.44  (-. (p303 zenon_X1))
% 1.11/1.44  (-. (p202 Tau_0))
% 1.11/1.44  (zenon_Vca != zenon_Vja)
% 1.11/1.44  (-. (p101 zenon_X1))
% 1.11/1.44  (r1 Tau_0 zenon_Vo)
% 1.11/1.44  (zenon_Vsa != zenon_Vja)
% 1.11/1.44  (-. (p105 zenon_Vfa))
% 1.11/1.44  (-. (p205 zenon_Vs))
% 1.11/1.44  (zenon_Vr != zenon_Vja)
% 1.11/1.44  (zenon_Vya != zenon_Vy)
% 1.11/1.44  (-. (p301 Tau_0))
% 1.11/1.44  (r1 zenon_X1 zenon_Vba)
% 1.11/1.44  (zenon_Vya != zenon_Vna)
% 1.11/1.44  (-. (p103 zenon_Vcb))
% 1.11/1.44  (zenon_Veb != zenon_Vda)
% 1.11/1.44  (-. (p203 zenon_Vva))
% 1.11/1.44  (zenon_Vga != zenon_Vna)
% 1.11/1.44  (-. (p305 zenon_Vca))
% 1.11/1.44  (zenon_Vca != zenon_Vna)
% 1.11/1.44  (-. (p201 zenon_X1))
% 1.11/1.44  (-. (p501 zenon_X1))
% 1.11/1.44  (zenon_Vma != zenon_Vfa)
% 1.11/1.44  (r1 zenon_X1 zenon_Vsa)
% 1.11/1.44  (p404 Tau_0)
% 1.11/1.44  (-. (p502 zenon_X1))
% 1.11/1.44  (-. (p103 zenon_Vza))
% 1.11/1.44  (-. (p201 Tau_0))
% 1.11/1.44  (-. (p302 zenon_X1))
% 1.11/1.44  (zenon_Vm != zenon_Vba)
% 1.11/1.44  (r1 zenon_X1 zenon_Vva)
% 1.11/1.44  (zenon_Veb != zenon_Vba)
% 1.11/1.44  (zenon_Vua != zenon_Vba)
% 1.11/1.44  (zenon_Vea != zenon_Vja)
% 1.11/1.44  (-. (p405 zenon_Vaa))
% 1.11/1.44  (zenon_Vga != zenon_Vja)
% 1.11/1.44  (zenon_Veb != zenon_Vna)
% 1.11/1.44  (-. (p405 zenon_Vm))
% 1.11/1.44  (zenon_Vea != zenon_Vfa)
% 1.11/1.44  (r1 Tau_0 zenon_Vs)
% 1.11/1.44  (r1 zenon_X1 zenon_Vv)
% 1.11/1.44  (zenon_X6 != zenon_Vja)
% 1.11/1.44  (zenon_Vcb != zenon_Vfa)
% 1.11/1.44  (-. (p105 zenon_Vda))
% 1.11/1.44  (zenon_Vs != zenon_Vba)
% 1.11/1.44  (zenon_Vo != zenon_Vba)
% 1.11/1.44  (-. (p305 zenon_Vr))
% 1.11/1.44  (p204 zenon_X6)
% 1.11/1.44  (zenon_Vx != zenon_Vy)
% 1.11/1.44  (zenon_Vya != zenon_Vda)
% 1.11/1.44  (zenon_X9 != zenon_Vy)
% 1.11/1.44  (zenon_Vca != zenon_Vfa)
% 1.11/1.44  (zenon_Vma != zenon_Vja)
% 1.11/1.44  (zenon_Vm != zenon_Vda)
% 1.11/1.44  (zenon_Vgb != zenon_Vy)
% 1.11/1.44  (zenon_Vsa != zenon_Vda)
% 1.11/1.44  (zenon_Vga != zenon_Vba)
% 1.11/1.44  (r1 zenon_X1 zenon_Vga)
% 1.11/1.44  (zenon_Vya != zenon_Vja)
% 1.11/1.44  (r1 zenon_X1 zenon_Vx)
% 1.11/1.44  (zenon_X9 != zenon_Vda)
% 1.11/1.44  (-. (p503 Tau_0))
% 1.11/1.44  (zenon_X9 != zenon_Vba)
% 1.11/1.44  (zenon_Vcb != zenon_Vba)
% 1.11/1.44  (r1 Tau_0 zenon_Vm)
% 1.11/1.44  (zenon_Vv != zenon_Vba)
% 1.11/1.44  (r1 zenon_X1 zenon_Vfb)
% 1.11/1.44  (zenon_Vr != zenon_Vda)
% 1.11/1.44  (zenon_Vs != zenon_Vna)
% 1.11/1.44  (-. (p203 zenon_Vya))
% 1.11/1.44  (zenon_Veb != zenon_Vja)
% 1.11/1.44  (-. (p505 zenon_X1))
% 1.11/1.44  (-. (p304 zenon_Vga))
% 1.11/1.44  (zenon_Vea != zenon_Vda)
% 1.11/1.44  (-. (p501 Tau_0))
% 1.11/1.44  (-. (p402 Tau_0))
% 1.11/1.44  (zenon_Vv != zenon_Vja)
% 1.11/1.44  (zenon_Vma != zenon_Vna)
% 1.11/1.44  (zenon_Vaa != zenon_Vfa)
% 1.11/1.44  (-. (p504 Tau_0))
% 1.11/1.44  (zenon_Vr != zenon_Vba)
% 1.11/1.44  (-. (p602 Tau_0))
% 1.11/1.44  (r1 zenon_X1 zenon_Vs)
% 1.11/1.44  (-. (p105 zenon_Vy))
% 1.11/1.44  (r1 Tau_0 zenon_Vr)
% 1.11/1.44  (zenon_Vv != zenon_Vda)
% 1.11/1.44  (zenon_Vua != zenon_Vja)
% 1.11/1.44  (zenon_Vx != zenon_Vba)
% 1.11/1.44  (-. (p505 Tau_0))
% 1.11/1.44  (zenon_Vsa != zenon_Vfa)
% 1.11/1.44  (-. (p205 zenon_Vx))
% 1.11/1.44  (zenon_Veb != zenon_Vfa)
% 1.11/1.44  (-. (p503 zenon_X1))
% 1.11/1.44  (zenon_Vo != zenon_Vja)
% 1.11/1.44  (zenon_Vua != zenon_Vy)
% 1.11/1.44  (zenon_Vcb != zenon_Vja)
% 1.11/1.44  (zenon_Vca != zenon_Vda)
% 1.11/1.44  (zenon_Vga != zenon_Vda)
% 1.11/1.44  (zenon_Vua != zenon_Vda)
% 1.11/1.44  (r1 zenon_X1 zenon_Vr)
% 1.11/1.44  (-. (p603 Tau_0))
% 1.11/1.44  (-. (p104 zenon_Voa))
% 1.11/1.44  (zenon_Vcb != zenon_Vna)
% 1.11/1.44  (r1 Tau_0 zenon_Vx)
% 1.11/1.44  (r1 Tau_0 zenon_Vaa)
% 1.11/1.44  (r1 Tau_0 zenon_Vca)
% 1.11/1.44  (r1 Tau_0 zenon_Vea)
% 1.11/1.44  (r1 Tau_0 zenon_Vga)
% 1.11/1.44  (r1 Tau_0 zenon_Vma)
% 1.11/1.44  (r1 Tau_0 zenon_Vsa)
% 1.11/1.44  (r1 Tau_0 zenon_Vua)
% 1.11/1.44  (r1 Tau_0 zenon_Vya)
% 1.11/1.44  (r1 Tau_0 zenon_Vcb)
% 1.11/1.44  (r1 Tau_0 zenon_Veb)
% 1.11/1.44  (r1 Tau_0 zenon_Vgb)
% 1.11/1.44  (zenon_Vaa != zenon_Vba)
% 1.11/1.44  (p502 Tau_0)
% 1.11/1.44  (p303 Tau_0)
% 1.11/1.44  (zenon_X6 != zenon_Vna)
% 1.11/1.44  (zenon_Vsa != zenon_Vna)
% 1.11/1.44  (-. (p101 Tau_0))
% 1.11/1.44  (zenon_Vgb != zenon_Vna)
% 1.11/1.44  (zenon_Vga != zenon_Vfa)
% 1.11/1.44  (zenon_Veb != zenon_Vy)
% 1.11/1.44  (zenon_Vea != zenon_Vba)
% 1.11/1.44  (zenon_Vgb != zenon_Vja)
% 1.11/1.44  (-. (p403 zenon_X1))
% 1.11/1.44  (-. (p102 zenon_Vfb))
% 1.11/1.44  (r1 zenon_X1 zenon_Vm)
% 1.11/1.44  (zenon_Vcb != zenon_Vda)
% 1.11/1.44  (zenon_Vs != zenon_Vja)
% 1.11/1.44  (-. (p301 zenon_X1))
% 1.11/1.44  (zenon_Vca != zenon_Vy)
% 1.11/1.44  (-. (p403 Tau_0))
% 1.11/1.44  (r1 zenon_X1 zenon_Vua)
% 1.11/1.44  (zenon_Vya != zenon_Vfa)
% 1.11/1.44  (zenon_Vx != zenon_Vja)
% 1.11/1.44  (r1 zenon_X1 zenon_Vja)
% 1.11/1.44  (zenon_Vr != zenon_Vna)
% 1.11/1.44  (zenon_Vm != zenon_Vfa)
% 1.11/1.44  (zenon_Vsa != zenon_Vy)
% 1.11/1.44  (zenon_Vo != zenon_Vy)
% 1.11/1.44  (zenon_Vua != zenon_Vna)
% 1.11/1.44  (zenon_Vua != zenon_Vfa)
% 1.11/1.44  (p105 zenon_X9)
% 1.11/1.44  *)
% 1.11/1.44  (* NO-PROOF *)
% 1.11/1.44  % SZS status GaveUp
% 1.11/1.44  Number of rewrites on terms: 0
% 1.11/1.44  Number of rewrites on props: 21
% 1.11/1.44  nodes searched: 8017
% 1.11/1.44  max branch formulas: 503
% 1.11/1.44  proof nodes created: 385
% 1.11/1.44  formulas created: 15942
% 1.11/1.44  
%------------------------------------------------------------------------------