%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : KRS041+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n018.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.18s 0.41s % Output : Saturation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : KRS041+1 : TPTP v8.1.0. Released v3.1.0. % 0.08/0.13 % Command : metis --show proof --show saturation %s % 0.12/0.34 % Computer : n018.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 : 600 % 0.12/0.34 % DateTime : Tue Jun 7 20:49:36 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.18/0.41 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.41 % 0.18/0.41 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.41 |- ~cowlNothing $X % 0.18/0.41 |- cowlThing $X % 0.18/0.41 |- ~xsd_integer $X \/ ~xsd_string $X % 0.18/0.41 |- xsd_integer $X \/ xsd_string $X % 0.18/0.41 |- ~cTest $X \/ cplus2 $X \/ cplus3 $X \/ cplus6 $X % 0.18/0.41 |- ~cTest $X \/ cplus3 $X \/ cplus6 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus8 $X \/ cplus4 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus3 $X \/ cminus6 $X \/ cminus8 $X % 0.18/0.41 |- ~cTest $X \/ cminus7 $X \/ cminus9 $X \/ cplus5 $X % 0.18/0.41 |- ~cTest $X \/ cminus5 $X \/ cminus7 $X \/ cplus1 $X % 0.18/0.41 |- ~cTest $X \/ cminus5 $X \/ cplus4 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus3 $X \/ cplus6 $X \/ cplus8 $X % 0.18/0.41 |- ~cTest $X \/ cminus3 $X \/ cplus1 $X \/ cplus9 $X % 0.18/0.41 |- ~cTest $X \/ cminus2 $X \/ cplus5 $X \/ cplus6 $X % 0.18/0.41 |- ~cTest $X \/ cminus1 $X \/ cminus8 $X \/ cplus9 $X % 0.18/0.41 |- ~cTest $X \/ cminus1 $X \/ cplus5 $X \/ cplus8 $X % 0.18/0.41 |- ~cTest $X \/ cminus3 $X \/ cminus5 $X \/ cplus4 $X % 0.18/0.41 |- ~cTest $X \/ cminus5 $X \/ cplus3 $X \/ cplus8 $X % 0.18/0.41 |- ~cTest $X \/ cminus1 $X \/ cminus2 $X \/ cplus9 $X % 0.18/0.41 |- ~cTest $X \/ cminus8 $X \/ cminus9 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus2 $X \/ cminus4 $X \/ cminus9 $X % 0.18/0.41 |- ~cTest $X \/ cminus2 $X \/ cplus3 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus2 $X \/ cminus3 $X \/ cminus7 $X % 0.18/0.41 |- ~cTest $X \/ cplus4 $X \/ cplus5 $X \/ cplus8 $X % 0.18/0.41 |- ~cTest $X \/ cplus2 $X \/ cplus5 $X \/ cplus8 $X % 0.18/0.41 |- ~cTest $X \/ cminus2 $X \/ cminus8 $X \/ cminus9 $X % 0.18/0.41 |- ~cTest $X \/ cminus6 $X \/ cplus1 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus7 $X \/ cminus9 $X \/ cplus3 $X % 0.18/0.41 |- ~cTest $X \/ cminus2 $X \/ cminus9 $X \/ cplus1 $X % 0.18/0.41 |- ~cTest $X \/ cminus7 $X \/ cplus5 $X \/ cplus6 $X % 0.18/0.41 |- ~cTest $X \/ cminus3 $X \/ cminus6 $X \/ cplus2 $X % 0.18/0.41 |- ~cTest $X \/ cminus3 $X \/ cplus2 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus1 $X \/ cplus6 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus1 $X \/ cminus2 $X \/ cplus3 $X % 0.18/0.41 |- ~cTest $X \/ cminus6 $X \/ cplus3 $X \/ cplus8 $X % 0.18/0.41 |- ~cTest $X \/ cminus8 $X \/ cminus9 $X \/ cplus2 $X % 0.18/0.41 |- ~cTest $X \/ cminus1 $X \/ cplus2 $X \/ cplus3 $X % 0.18/0.41 |- ~cTest $X \/ cminus7 $X \/ cplus3 $X \/ cplus8 $X % 0.18/0.41 |- ~cTest $X \/ cminus5 $X \/ cminus6 $X \/ cminus8 $X % 0.18/0.41 |- ~cTest $X \/ cminus7 $X \/ cplus2 $X \/ cplus5 $X % 0.18/0.41 |- ~cTest $X \/ cminus2 $X \/ cminus5 $X \/ cplus3 $X % 0.18/0.41 |- ~cTest $X \/ cminus1 $X \/ cminus9 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus9 $X \/ cplus3 $X \/ cplus6 $X % 0.18/0.41 |- ~cTest $X \/ cminus3 $X \/ cminus8 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus1 $X \/ cminus4 $X \/ cplus7 $X % 0.18/0.41 |- ~cTest $X \/ cminus8 $X \/ cplus1 $X \/ cplus2 $X % 0.18/0.41 |- ~cTest $X \/ cminus4 $X \/ cminus6 $X \/ cplus8 $X % 0.18/0.41 |- ~cTest $X \/ cplus1 $X \/ cplus4 $X \/ cplus6 $X % 0.18/0.41 |- ~cTest $X \/ cminus7 $X \/ cplus4 $X \/ cplus8 $X % 0.18/0.41 |- cTest i2003_11_14_17_16_07145 % 0.18/0.41 |- ~cminus8 $X \/ ~cplus8 $X % 0.18/0.41 |- ~cminus9 $X \/ ~cplus9 $X % 0.18/0.41 |- ~cminus4 $X \/ ~cplus4 $X % 0.18/0.41 |- ~cminus7 $X \/ ~cplus7 $X % 0.18/0.41 |- ~cminus3 $X \/ ~cplus3 $X % 0.18/0.41 |- ~cminus5 $X \/ ~cplus5 $X % 0.18/0.41 |- ~cminus2 $X \/ ~cplus2 $X % 0.18/0.41 |- ~cminus1 $X \/ ~cplus1 $X % 0.18/0.41 |- ~cminus6 $X \/ ~cplus6 $X % 0.18/0.41 |- cminus8 i2003_11_14_17_16_07145 \/ cplus4 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus7 i2003_11_14_17_16_07145 % 0.18/0.41 |- ~cminus7 i2003_11_14_17_16_07145 \/ cminus8 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus4 i2003_11_14_17_16_07145 % 0.18/0.41 |- cminus8 i2003_11_14_17_16_07145 \/ cminus9 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus7 i2003_11_14_17_16_07145 % 0.18/0.41 |- ~cminus7 i2003_11_14_17_16_07145 \/ cminus8 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cminus9 i2003_11_14_17_16_07145 % 0.18/0.41 |- cminus2 i2003_11_14_17_16_07145 \/ cplus3 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus7 i2003_11_14_17_16_07145 % 0.18/0.41 |- ~cminus7 i2003_11_14_17_16_07145 \/ cminus2 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus3 i2003_11_14_17_16_07145 % 0.18/0.41 |- cplus2 i2003_11_14_17_16_07145 \/ cplus3 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus6 i2003_11_14_17_16_07145 % 0.18/0.41 |- ~cminus6 i2003_11_14_17_16_07145 \/ cplus2 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus3 i2003_11_14_17_16_07145 % 0.18/0.41 |- cplus3 i2003_11_14_17_16_07145 \/ cplus6 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus7 i2003_11_14_17_16_07145 % 0.18/0.41 |- ~cminus7 i2003_11_14_17_16_07145 \/ cplus3 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus6 i2003_11_14_17_16_07145 % 0.18/0.41 |- cminus2 i2003_11_14_17_16_07145 \/ cplus5 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus6 i2003_11_14_17_16_07145 % 0.18/0.41 |- ~cminus6 i2003_11_14_17_16_07145 \/ cminus2 i2003_11_14_17_16_07145 \/ % 0.18/0.41 cplus5 i2003_11_14_17_16_07145 % 0.18/0.42 |- cplus4 i2003_11_14_17_16_07145 \/ cplus5 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus8 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus8 i2003_11_14_17_16_07145 \/ cplus4 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus5 i2003_11_14_17_16_07145 % 0.18/0.42 |- cplus2 i2003_11_14_17_16_07145 \/ cplus5 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus8 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus8 i2003_11_14_17_16_07145 \/ cplus2 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus5 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus6 i2003_11_14_17_16_07145 \/ cplus1 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus7 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus7 i2003_11_14_17_16_07145 \/ cminus6 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus1 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus7 i2003_11_14_17_16_07145 \/ cplus5 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus6 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus6 i2003_11_14_17_16_07145 \/ cminus7 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus5 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus6 i2003_11_14_17_16_07145 \/ cplus3 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus8 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus8 i2003_11_14_17_16_07145 \/ cminus6 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus3 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus8 i2003_11_14_17_16_07145 \/ cminus9 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus2 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus2 i2003_11_14_17_16_07145 \/ cminus8 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cminus9 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus1 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus2 i2003_11_14_17_16_07145 \/ cminus9 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus7 i2003_11_14_17_16_07145 \/ cplus3 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus8 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus8 i2003_11_14_17_16_07145 \/ cminus7 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus3 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus9 i2003_11_14_17_16_07145 \/ cplus3 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus6 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus6 i2003_11_14_17_16_07145 \/ cminus9 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus3 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus3 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus5 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus7 i2003_11_14_17_16_07145 \/ cminus9 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus7 i2003_11_14_17_16_07145 \/ cplus2 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus2 i2003_11_14_17_16_07145 \/ cminus7 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus8 i2003_11_14_17_16_07145 \/ cplus1 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus2 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus2 i2003_11_14_17_16_07145 \/ cminus8 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus1 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus4 i2003_11_14_17_16_07145 \/ cminus6 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus8 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus8 i2003_11_14_17_16_07145 \/ cminus4 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cminus6 i2003_11_14_17_16_07145 % 0.18/0.42 |- cplus1 i2003_11_14_17_16_07145 \/ cplus4 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus6 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus6 i2003_11_14_17_16_07145 \/ cplus1 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus4 i2003_11_14_17_16_07145 % 0.18/0.42 |- cminus7 i2003_11_14_17_16_07145 \/ cplus4 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus8 i2003_11_14_17_16_07145 % 0.18/0.42 |- ~cminus8 i2003_11_14_17_16_07145 \/ cminus7 i2003_11_14_17_16_07145 \/ % 0.18/0.42 cplus4 i2003_11_14_17_16_07145 % 0.18/0.42 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.42 %------------------------------------------------------------------------------