↑ Up

Metis---2.4.SAT-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : KRS043+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n029.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 : Sun Jul 17 03:18:31 EDT 2022

% Result   : Satisfiable 0.19s 0.46s
% Output   : Saturation 0.19s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : KRS043+1 : TPTP v8.1.0. Released v3.1.0.
% 0.11/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.33  % Computer : n029.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 Jun  7 20:45:20 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.19/0.46  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46  
% 0.19/0.46  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46  |- ~cowlNothing $X
% 0.19/0.46  |- cowlThing $X
% 0.19/0.46  |- ~xsd_integer $X \/ ~xsd_string $X
% 0.19/0.46  |- xsd_integer $X \/ xsd_string $X
% 0.19/0.46  |- ~cSatisfiable $X \/ ca_Ax14 (skolemFOFtoCNF_Y $X)
% 0.19/0.46  |- ~cSatisfiable $X \/ rinvR $X (skolemFOFtoCNF_Y $X)
% 0.19/0.46  |- ~ca_Ax14 $Y \/ ~rinvR $X $Y \/ cSatisfiable $X
% 0.19/0.46  |- ~cp1 $X \/ ca_Cx1 $X
% 0.19/0.46  |- ~cp2 $X \/ ra_Px5 $X (skolemFOFtoCNF_Y0 $X)
% 0.19/0.46  |- ~ra_Px5 $X $Y0 \/ cp2 $X
% 0.19/0.46  |- ~cp2 $X \/ ca_Cx2 $X
% 0.19/0.46  |- ~cp2xcomp $X \/ ~ra_Px5 $X $Y
% 0.19/0.46  |- cp2xcomp $X \/ ra_Px5 $X (skolemFOFtoCNF_Y_1 $X)
% 0.19/0.46  |- ~cp3 $X \/ ra_Px6 $X (skolemFOFtoCNF_Y0_1 $X)
% 0.19/0.46  |- ~ra_Px6 $X $Y0 \/ cp3 $X
% 0.19/0.46  |- ~cp3 $X \/ ca_Cx3 $X
% 0.19/0.46  |- ~cp3xcomp $X \/ ~ra_Px6 $X $Y
% 0.19/0.46  |- cp3xcomp $X \/ ra_Px6 $X (skolemFOFtoCNF_Y_2 $X)
% 0.19/0.46  |- ~cp4 $X \/ ~ra_Px7 $X $Y
% 0.19/0.46  |- cp4 $X \/ ra_Px7 $X (skolemFOFtoCNF_Y_3 $X)
% 0.19/0.46  |- ~cp4 $X \/ cp5xcomp $X
% 0.19/0.46  |- ~cp4xcomp $X \/ ra_Px7 $X (skolemFOFtoCNF_Y0_2 $X)
% 0.19/0.46  |- ~ra_Px7 $X $Y0 \/ cp4xcomp $X
% 0.19/0.46  |- ~cp5 $X \/ ~ra_Px4 $X $Y
% 0.19/0.46  |- cp5 $X \/ ra_Px4 $X (skolemFOFtoCNF_Y_4 $X)
% 0.19/0.46  |- ~cp5xcomp $X \/ ra_Px4 $X (skolemFOFtoCNF_Y0_3 $X)
% 0.19/0.46  |- ~ra_Px4 $X $Y0 \/ cp5xcomp $X
% 0.19/0.46  |- ~ca_Ax14 $X \/ cp1 (skolemFOFtoCNF_Y_5 $X)
% 0.19/0.46  |- ~ca_Ax14 $X \/ rr $X (skolemFOFtoCNF_Y_5 $X)
% 0.19/0.46  |- ~(skolemFOFtoCNF_Y0_4 $X = skolemFOFtoCNF_Y1 $X) \/ ~cp1 $Y \/
% 0.19/0.46     ~rr $X $Y \/ ca_Ax14 $X
% 0.19/0.46  |- ~ca_Ax14 $X \/ ~rr $X $Y0 \/ ~rr $X $Y1 \/ $Y0 = $Y1
% 0.19/0.46  |- ~cp1 $Y \/ ~rr $X $Y \/ ca_Ax14 $X \/ rr $X (skolemFOFtoCNF_Y0_4 $X)
% 0.19/0.46  |- ~cp1 $Y \/ ~rr $X $Y \/ ca_Ax14 $X \/ rr $X (skolemFOFtoCNF_Y1 $X)
% 0.19/0.46  |- ~ca_Cx1 $X \/ ra_Px1 $X (skolemFOFtoCNF_Y0_5 $X)
% 0.19/0.46  |- ~ra_Px1 $X $Y0 \/ ca_Cx1 $X
% 0.19/0.46  |- ~ca_Cx1 $X \/ cp2xcomp $X
% 0.19/0.46  |- ~ca_Cx1 $X \/ cp3xcomp $X
% 0.19/0.46  |- ~ca_Cx1 $X \/ cp4xcomp $X
% 0.19/0.46  |- ~ca_Cx1 $X \/ cp5xcomp $X
% 0.19/0.46  |- ~cp2xcomp $X \/ ~cp3xcomp $X \/ ~cp4xcomp $X \/ ~cp5xcomp $X \/
% 0.19/0.46     ca_Cx1 $X
% 0.19/0.46  |- ~ca_Cx1xcomp $X \/ ~ra_Px1 $X $Y
% 0.19/0.46  |- ca_Cx1xcomp $X \/ ra_Px1 $X (skolemFOFtoCNF_Y_6 $X)
% 0.19/0.46  |- ~ca_Cx2 $X \/ ~ra_Px2 $X $Y
% 0.19/0.46  |- ca_Cx2 $X \/ ra_Px2 $X (skolemFOFtoCNF_Y_7 $X)
% 0.19/0.46  |- ~ca_Cx2 $X \/ cp3xcomp $X
% 0.19/0.46  |- ~ca_Cx2 $X \/ cp4xcomp $X
% 0.19/0.46  |- ~ca_Cx2 $X \/ cp5xcomp $X
% 0.19/0.46  |- ~cp3xcomp $X \/ ~cp4xcomp $X \/ ~cp5xcomp $X \/ ca_Cx2 $X
% 0.19/0.46  |- ~ca_Cx2xcomp $X \/ ra_Px2 $X (skolemFOFtoCNF_Y0_6 $X)
% 0.19/0.46  |- ~ra_Px2 $X $Y0 \/ ca_Cx2xcomp $X
% 0.19/0.46  |- ~ca_Cx3 $X \/ cp4xcomp $X
% 0.19/0.46  |- ~ca_Cx3 $X \/ cp5xcomp $X
% 0.19/0.46  |- ~cp4xcomp $X \/ ~cp5xcomp $X \/ ca_Cx3 $X
% 0.19/0.46  |- ~ca_Cx3 $X \/ ~ra_Px3 $X $Y
% 0.19/0.46  |- ca_Cx3 $X \/ ra_Px3 $X (skolemFOFtoCNF_Y_8 $X)
% 0.19/0.46  |- ~ca_Cx3xcomp $X \/ ra_Px3 $X (skolemFOFtoCNF_Y0_7 $X)
% 0.19/0.46  |- ~ra_Px3 $X $Y0 \/ ca_Cx3xcomp $X
% 0.19/0.46  |- ~rinvR $X $Y \/ rr $Y $X
% 0.19/0.46  |- ~rr $Y $X \/ rinvR $X $Y
% 0.19/0.46  |- cSatisfiable i2003_11_14_17_16_14536
% 0.19/0.46  |- ca_Ax14 (skolemFOFtoCNF_Y i2003_11_14_17_16_14536)
% 0.19/0.46  |- cp1 i2003_11_14_17_16_14536
% 0.19/0.46  |- ca_Cx1 i2003_11_14_17_16_14536
% 0.19/0.46  |- cp5xcomp i2003_11_14_17_16_14536
% 0.19/0.46  |- cp4xcomp i2003_11_14_17_16_14536
% 0.19/0.46  |- cp3xcomp i2003_11_14_17_16_14536
% 0.19/0.46  |- cp2xcomp i2003_11_14_17_16_14536
% 0.19/0.46  |- rinvR i2003_11_14_17_16_14536 (skolemFOFtoCNF_Y i2003_11_14_17_16_14536)
% 0.19/0.46  |- ra_Px7 i2003_11_14_17_16_14536
% 0.19/0.46       (skolemFOFtoCNF_Y0_2 i2003_11_14_17_16_14536)
% 0.19/0.46  |- ra_Px4 i2003_11_14_17_16_14536
% 0.19/0.46       (skolemFOFtoCNF_Y0_3 i2003_11_14_17_16_14536)
% 0.19/0.46  |- ra_Px1 i2003_11_14_17_16_14536
% 0.19/0.46       (skolemFOFtoCNF_Y0_5 i2003_11_14_17_16_14536)
% 0.19/0.46  |- cp2 $_35 \/ cp2xcomp $_35
% 0.19/0.46  |- cp3 $_40 \/ cp3xcomp $_40
% 0.19/0.46  |- ~cp4 i2003_11_14_17_16_14536
% 0.19/0.46  |- cp4 $_47 \/ cp4xcomp $_47
% 0.19/0.46  |- cp4 $_49 \/ ra_Px7 $_49 (skolemFOFtoCNF_Y0_2 $_49)
% 0.19/0.46  |- ~cp5 i2003_11_14_17_16_14536
% 0.19/0.46  |- cp5 $_53 \/ cp5xcomp $_53
% 0.19/0.46  |- cp5 $_55 \/ ra_Px4 $_55 (skolemFOFtoCNF_Y0_3 $_55)
% 0.19/0.46  |- ca_Cx1 $_57 \/ ca_Cx1xcomp $_57
% 0.19/0.46  |- ~ca_Cx1xcomp i2003_11_14_17_16_14536
% 0.19/0.46  |- ca_Cx2 $_64 \/ ca_Cx2xcomp $_64
% 0.19/0.46  |- ca_Cx2 $_66 \/ ra_Px2 $_66 (skolemFOFtoCNF_Y0_6 $_66)
% 0.19/0.46  |- ca_Cx3 $_70 \/ ca_Cx3xcomp $_70
% 0.19/0.46  |- ca_Cx3 $_72 \/ ra_Px3 $_72 (skolemFOFtoCNF_Y0_7 $_72)
% 0.19/0.46  |- ca_Cx3 i2003_11_14_17_16_14536
% 0.19/0.46  |- ~cp4xcomp $_74 \/ ca_Cx3 $_74 \/ cp5 $_74
% 0.19/0.46  |- rr (skolemFOFtoCNF_Y i2003_11_14_17_16_14536) i2003_11_14_17_16_14536
% 0.19/0.46  |- ca_Cx3 $_79 \/ cp4 $_79 \/ cp5 $_79
% 0.19/0.46  |- ca_Cx2 i2003_11_14_17_16_14536
% 0.19/0.46  |- ~cp3xcomp $_81 \/ ~cp4xcomp $_81 \/ ca_Cx2 $_81 \/ cp5 $_81
% 0.19/0.46  |- ~cp3xcomp $_84 \/ ca_Cx2 $_84 \/ cp4 $_84 \/ cp5 $_84
% 0.19/0.46  |- ca_Cx2 $_85 \/ cp3 $_85 \/ cp4 $_85 \/ cp5 $_85
% 0.19/0.46  |- ~cp2xcomp $_87 \/ ~cp3xcomp $_87 \/ ~cp4xcomp $_87 \/ ca_Cx1 $_87 \/
% 0.19/0.46     cp5 $_87
% 0.19/0.46  |- ~cp2xcomp $_88 \/ ~cp3xcomp $_88 \/ ca_Cx1 $_88 \/ cp4 $_88 \/ cp5 $_88
% 0.19/0.46  |- ~cp2xcomp $_89 \/ ca_Cx1 $_89 \/ cp3 $_89 \/ cp4 $_89 \/ cp5 $_89
% 0.19/0.46  |- ca_Cx1 $_90 \/ cp2 $_90 \/ cp3 $_90 \/ cp4 $_90 \/ cp5 $_90
% 0.19/0.46  |- ~rr (skolemFOFtoCNF_Y i2003_11_14_17_16_14536) $_99 \/
% 0.19/0.46     $_99 = i2003_11_14_17_16_14536
% 0.19/0.46  |- skolemFOFtoCNF_Y_5 (skolemFOFtoCNF_Y i2003_11_14_17_16_14536) =
% 0.19/0.46     i2003_11_14_17_16_14536
% 0.19/0.46  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46  
%------------------------------------------------------------------------------