%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : KRS040+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n032.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 : 0s % DateTime : Sun Jul 17 02:50:59 EDT 2022 % Result : Satisfiable 0.13s 0.44s % Output : Model 0.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.09 % Problem : KRS040+1 : TPTP v8.1.0. Released v3.1.0. % 0.05/0.10 % Command : darwin -pl 0 -pmc true -to %d %s % 0.09/0.29 % Computer : n032.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % DateTime : Tue Jun 7 18:08:36 EDT 2022 % 0.09/0.29 % CPUTime : % 0.09/0.29 Defaulting to tptp format. % 0.13/0.44 SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.13/0.44 % 0.13/0.44 MODEL (CONTEXT): % 0.13/0.44 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.13/0.44 -__-v__(=0) % 0.13/0.44 +(_0 = _0) % 0.13/0.44 +(iminus3 = iminus1) % 0.13/0.44 +(iminus3 = iplus4) % 0.13/0.44 +(iminus3 = iplus7) % 0.13/0.44 +(iminus3 = iplus6) % 0.13/0.44 +(iminus3 = iminus5) % 0.13/0.44 +(iminus3 = iplus2) % 0.13/0.44 +(iminus3 = iplus8) % 0.13/0.44 +(iminus3 = iminus9) % 0.13/0.44 +(iminus3 = iT) % 0.13/0.44 +(iplus3 = iplus1) % 0.13/0.44 +(iplus3 = iminus4) % 0.13/0.44 +(iplus3 = iminus7) % 0.13/0.44 +(iplus3 = iminus6) % 0.13/0.44 +(iplus3 = iplus5) % 0.13/0.44 +(iplus3 = iminus2) % 0.13/0.44 +(iplus3 = iminus8) % 0.13/0.44 +(iplus3 = iplus9) % 0.13/0.44 +(iplus3 = iF) % 0.13/0.44 +(iminus1 = iminus3) % 0.13/0.44 +(iminus1 = iplus4) % 0.13/0.44 +(iminus1 = iplus7) % 0.13/0.44 +(iminus1 = iplus6) % 0.13/0.44 +(iminus1 = iminus5) % 0.13/0.44 +(iminus1 = iplus2) % 0.13/0.44 +(iminus1 = iplus8) % 0.13/0.44 +(iminus1 = iminus9) % 0.13/0.44 +(iminus1 = iT) % 0.13/0.44 +(iplus1 = iplus3) % 0.13/0.44 +(iplus1 = iminus4) % 0.13/0.44 +(iplus1 = iminus7) % 0.13/0.44 +(iplus1 = iminus6) % 0.13/0.44 +(iplus1 = iplus5) % 0.13/0.44 +(iplus1 = iminus2) % 0.13/0.44 +(iplus1 = iminus8) % 0.13/0.44 +(iplus1 = iplus9) % 0.13/0.44 +(iplus1 = iF) % 0.13/0.44 +(iplus4 = iminus3) % 0.13/0.44 +(iplus4 = iminus1) % 0.13/0.44 +(iplus4 = iplus7) % 0.13/0.44 +(iplus4 = iplus6) % 0.13/0.44 +(iplus4 = iminus5) % 0.13/0.44 +(iplus4 = iplus2) % 0.13/0.44 +(iplus4 = iplus8) % 0.13/0.44 +(iplus4 = iminus9) % 0.13/0.44 +(iplus4 = iT) % 0.13/0.44 +(iminus4 = iplus3) % 0.13/0.44 +(iminus4 = iplus1) % 0.13/0.44 +(iminus4 = iminus7) % 0.13/0.44 +(iminus4 = iminus6) % 0.13/0.44 +(iminus4 = iplus5) % 0.13/0.44 +(iminus4 = iminus2) % 0.13/0.44 +(iminus4 = iminus8) % 0.13/0.44 +(iminus4 = iplus9) % 0.13/0.44 +(iminus4 = iF) % 0.13/0.44 +(iplus7 = iminus3) % 0.13/0.44 +(iplus7 = iminus1) % 0.13/0.44 +(iplus7 = iplus4) % 0.13/0.44 +(iplus7 = iplus6) % 0.13/0.44 +(iplus7 = iminus5) % 0.13/0.44 +(iplus7 = iplus2) % 0.13/0.44 +(iplus7 = iplus8) % 0.13/0.44 +(iplus7 = iminus9) % 0.13/0.44 +(iplus7 = iT) % 0.13/0.44 +(iminus7 = iplus3) % 0.13/0.44 +(iminus7 = iplus1) % 0.13/0.44 +(iminus7 = iminus4) % 0.13/0.44 +(iminus7 = iminus6) % 0.13/0.44 +(iminus7 = iplus5) % 0.13/0.44 +(iminus7 = iminus2) % 0.13/0.44 +(iminus7 = iminus8) % 0.13/0.44 +(iminus7 = iplus9) % 0.13/0.44 +(iminus7 = iF) % 0.13/0.44 +(iplus6 = iminus3) % 0.13/0.44 +(iplus6 = iminus1) % 0.13/0.44 +(iplus6 = iplus4) % 0.13/0.44 +(iplus6 = iplus7) % 0.13/0.44 +(iplus6 = iminus5) % 0.13/0.44 +(iplus6 = iplus2) % 0.13/0.44 +(iplus6 = iplus8) % 0.13/0.44 +(iplus6 = iminus9) % 0.13/0.44 +(iplus6 = iT) % 0.13/0.44 +(iminus6 = iplus3) % 0.13/0.44 +(iminus6 = iplus1) % 0.13/0.44 +(iminus6 = iminus4) % 0.13/0.44 +(iminus6 = iminus7) % 0.13/0.44 +(iminus6 = iplus5) % 0.13/0.44 +(iminus6 = iminus2) % 0.13/0.44 +(iminus6 = iminus8) % 0.13/0.44 +(iminus6 = iplus9) % 0.13/0.44 +(iminus6 = iF) % 0.13/0.44 +(iminus5 = iminus3) % 0.13/0.44 +(iminus5 = iminus1) % 0.13/0.44 +(iminus5 = iplus4) % 0.13/0.44 +(iminus5 = iplus7) % 0.13/0.44 +(iminus5 = iplus6) % 0.13/0.44 +(iminus5 = iplus2) % 0.13/0.44 +(iminus5 = iplus8) % 0.13/0.44 +(iminus5 = iminus9) % 0.13/0.44 +(iminus5 = iT) % 0.13/0.44 +(iplus5 = iplus3) % 0.13/0.44 +(iplus5 = iplus1) % 0.13/0.44 +(iplus5 = iminus4) % 0.13/0.44 +(iplus5 = iminus7) % 0.13/0.44 +(iplus5 = iminus6) % 0.13/0.44 +(iplus5 = iminus2) % 0.13/0.44 +(iplus5 = iminus8) % 0.13/0.44 +(iplus5 = iplus9) % 0.13/0.44 +(iplus5 = iF) % 0.13/0.44 +(iplus2 = iminus3) % 0.13/0.44 +(iplus2 = iminus1) % 0.13/0.44 +(iplus2 = iplus4) % 0.13/0.44 +(iplus2 = iplus7) % 0.13/0.44 +(iplus2 = iplus6) % 0.13/0.44 +(iplus2 = iminus5) % 0.13/0.44 +(iplus2 = iplus8) % 0.13/0.44 +(iplus2 = iminus9) % 0.13/0.44 +(iplus2 = iT) % 0.13/0.44 +(iminus2 = iplus3) % 0.13/0.44 +(iminus2 = iplus1) % 0.13/0.44 +(iminus2 = iminus4) % 0.13/0.44 +(iminus2 = iminus7) % 0.13/0.44 +(iminus2 = iminus6) % 0.13/0.44 +(iminus2 = iplus5) % 0.13/0.44 +(iminus2 = iminus8) % 0.13/0.44 +(iminus2 = iplus9) % 0.13/0.44 +(iminus2 = iF) % 0.13/0.44 +(iplus8 = iminus3) % 0.13/0.44 +(iplus8 = iminus1) % 0.13/0.44 +(iplus8 = iplus4) % 0.13/0.44 +(iplus8 = iplus7) % 0.13/0.44 +(iplus8 = iplus6) % 0.13/0.44 +(iplus8 = iminus5) % 0.13/0.44 +(iplus8 = iplus2) % 0.13/0.44 +(iplus8 = iminus9) % 0.13/0.44 +(iplus8 = iT) % 0.13/0.44 +(iminus8 = iplus3) % 0.13/0.44 +(iminus8 = iplus1) % 0.13/0.44 +(iminus8 = iminus4) % 0.13/0.44 +(iminus8 = iminus7) % 0.13/0.44 +(iminus8 = iminus6) % 0.13/0.44 +(iminus8 = iplus5) % 0.13/0.44 +(iminus8 = iminus2) % 0.13/0.44 +(iminus8 = iplus9) % 0.13/0.44 +(iminus8 = iF) % 0.13/0.44 +(iplus9 = iplus3) % 0.13/0.44 +(iplus9 = iplus1) % 0.13/0.44 +(iplus9 = iminus4) % 0.13/0.44 +(iplus9 = iminus7) % 0.13/0.44 +(iplus9 = iminus6) % 0.13/0.44 +(iplus9 = iplus5) % 0.13/0.44 +(iplus9 = iminus2) % 0.13/0.44 +(iplus9 = iminus8) % 0.13/0.44 +(iplus9 = iF) % 0.13/0.44 +(iminus9 = iminus3) % 0.13/0.44 +(iminus9 = iminus1) % 0.13/0.44 +(iminus9 = iplus4) % 0.13/0.44 +(iminus9 = iplus7) % 0.13/0.44 +(iminus9 = iplus6) % 0.13/0.44 +(iminus9 = iminus5) % 0.13/0.44 +(iminus9 = iplus2) % 0.13/0.44 +(iminus9 = iplus8) % 0.13/0.44 +(iminus9 = iT) % 0.13/0.44 +(iF = iplus3) % 0.13/0.44 +(iF = iplus1) % 0.13/0.44 +(iF = iminus4) % 0.13/0.44 +(iF = iminus7) % 0.13/0.44 +(iF = iminus6) % 0.13/0.44 +(iF = iplus5) % 0.13/0.44 +(iF = iminus2) % 0.13/0.44 +(iF = iminus8) % 0.13/0.44 +(iF = iplus9) % 0.13/0.44 +(iT = iminus3) % 0.13/0.44 +(iT = iminus1) % 0.13/0.44 +(iT = iplus4) % 0.13/0.44 +(iT = iplus7) % 0.13/0.44 +(iT = iplus6) % 0.13/0.44 +(iT = iminus5) % 0.13/0.44 +(iT = iplus2) % 0.13/0.44 +(iT = iplus8) % 0.13/0.44 +(iT = iminus9) % 0.13/0.44 -(iminus3 = iplus3) % 0.13/0.44 -(iminus3 = iplus1) % 0.13/0.44 -(iminus3 = iminus4) % 0.13/0.44 -(iminus3 = iminus7) % 0.13/0.44 -(iminus3 = iminus6) % 0.13/0.44 -(iminus3 = iplus5) % 0.13/0.44 -(iminus3 = iminus2) % 0.13/0.44 -(iminus3 = iminus8) % 0.13/0.44 -(iminus3 = iplus9) % 0.13/0.44 -(iminus3 = iF) % 0.13/0.44 -(iplus3 = iminus3) % 0.13/0.44 -(iplus3 = iminus1) % 0.13/0.44 -(iplus3 = iplus4) % 0.13/0.44 -(iplus3 = iplus7) % 0.13/0.44 -(iplus3 = iplus6) % 0.13/0.44 -(iplus3 = iminus5) % 0.13/0.44 -(iplus3 = iplus2) % 0.13/0.44 -(iplus3 = iplus8) % 0.13/0.44 -(iplus3 = iminus9) % 0.13/0.44 -(iplus3 = iT) % 0.13/0.44 -(iminus1 = iplus3) % 0.13/0.44 -(iminus1 = iplus1) % 0.13/0.44 -(iminus1 = iminus4) % 0.13/0.44 -(iminus1 = iminus7) % 0.13/0.44 -(iminus1 = iminus6) % 0.13/0.44 -(iminus1 = iplus5) % 0.13/0.44 -(iminus1 = iminus2) % 0.13/0.44 -(iminus1 = iminus8) % 0.13/0.44 -(iminus1 = iplus9) % 0.13/0.44 -(iminus1 = iF) % 0.13/0.44 -(iplus1 = iminus3) % 0.13/0.44 -(iplus1 = iminus1) % 0.13/0.44 -(iplus1 = iplus4) % 0.13/0.44 -(iplus1 = iplus7) % 0.13/0.44 -(iplus1 = iplus6) % 0.13/0.44 -(iplus1 = iminus5) % 0.13/0.44 -(iplus1 = iplus2) % 0.13/0.44 -(iplus1 = iplus8) % 0.13/0.44 -(iplus1 = iminus9) % 0.13/0.44 -(iplus1 = iT) % 0.13/0.44 -(iplus4 = iplus3) % 0.13/0.44 -(iplus4 = iplus1) % 0.13/0.44 -(iplus4 = iminus4) % 0.13/0.44 -(iplus4 = iminus7) % 0.13/0.44 -(iplus4 = iminus6) % 0.13/0.44 -(iplus4 = iplus5) % 0.13/0.44 -(iplus4 = iminus2) % 0.13/0.44 -(iplus4 = iminus8) % 0.13/0.44 -(iplus4 = iplus9) % 0.13/0.44 -(iplus4 = iF) % 0.13/0.44 -(iminus4 = iminus3) % 0.13/0.44 -(iminus4 = iminus1) % 0.13/0.44 -(iminus4 = iplus4) % 0.13/0.44 -(iminus4 = iplus7) % 0.13/0.44 -(iminus4 = iplus6) % 0.13/0.44 -(iminus4 = iminus5) % 0.13/0.44 -(iminus4 = iplus2) % 0.13/0.44 -(iminus4 = iplus8) % 0.13/0.44 -(iminus4 = iminus9) % 0.13/0.44 -(iminus4 = iT) % 0.13/0.44 -(iplus7 = iplus3) % 0.13/0.44 -(iplus7 = iplus1) % 0.13/0.44 -(iplus7 = iminus4) % 0.13/0.44 -(iplus7 = iminus7) % 0.13/0.44 -(iplus7 = iminus6) % 0.13/0.44 -(iplus7 = iplus5) % 0.13/0.44 -(iplus7 = iminus2) % 0.13/0.44 -(iplus7 = iminus8) % 0.13/0.44 -(iplus7 = iplus9) % 0.13/0.44 -(iplus7 = iF) % 0.13/0.44 -(iminus7 = iminus3) % 0.13/0.44 -(iminus7 = iminus1) % 0.13/0.44 -(iminus7 = iplus4) % 0.13/0.44 -(iminus7 = iplus7) % 0.13/0.44 -(iminus7 = iplus6) % 0.13/0.44 -(iminus7 = iminus5) % 0.13/0.44 -(iminus7 = iplus2) % 0.13/0.44 -(iminus7 = iplus8) % 0.13/0.44 -(iminus7 = iminus9) % 0.13/0.44 -(iminus7 = iT) % 0.13/0.44 -(iplus6 = iplus3) % 0.13/0.44 -(iplus6 = iplus1) % 0.13/0.44 -(iplus6 = iminus4) % 0.13/0.44 -(iplus6 = iminus7) % 0.13/0.44 -(iplus6 = iminus6) % 0.13/0.44 -(iplus6 = iplus5) % 0.13/0.44 -(iplus6 = iminus2) % 0.13/0.44 -(iplus6 = iminus8) % 0.13/0.44 -(iplus6 = iplus9) % 0.13/0.44 -(iplus6 = iF) % 0.13/0.44 -(iminus6 = iminus3) % 0.13/0.44 -(iminus6 = iminus1) % 0.13/0.44 -(iminus6 = iplus4) % 0.13/0.44 -(iminus6 = iplus7) % 0.13/0.44 -(iminus6 = iplus6) % 0.13/0.44 -(iminus6 = iminus5) % 0.13/0.44 -(iminus6 = iplus2) % 0.13/0.44 -(iminus6 = iplus8) % 0.13/0.44 -(iminus6 = iminus9) % 0.13/0.44 -(iminus6 = iT) % 0.13/0.44 -(iminus5 = iplus3) % 0.13/0.44 -(iminus5 = iplus1) % 0.13/0.44 -(iminus5 = iminus4) % 0.13/0.44 -(iminus5 = iminus7) % 0.13/0.44 -(iminus5 = iminus6) % 0.13/0.44 -(iminus5 = iplus5) % 0.13/0.44 -(iminus5 = iminus2) % 0.13/0.44 -(iminus5 = iminus8) % 0.13/0.44 -(iminus5 = iplus9) % 0.13/0.44 -(iminus5 = iF) % 0.13/0.44 -(iplus5 = iminus3) % 0.13/0.44 -(iplus5 = iminus1) % 0.13/0.44 -(iplus5 = iplus4) % 0.13/0.44 -(iplus5 = iplus7) % 0.13/0.44 -(iplus5 = iplus6) % 0.13/0.44 -(iplus5 = iminus5) % 0.13/0.44 -(iplus5 = iplus2) % 0.13/0.44 -(iplus5 = iplus8) % 0.13/0.44 -(iplus5 = iminus9) % 0.13/0.44 -(iplus5 = iT) % 0.13/0.44 -(iplus2 = iplus3) % 0.13/0.44 -(iplus2 = iplus1) % 0.13/0.44 -(iplus2 = iminus4) % 0.13/0.44 -(iplus2 = iminus7) % 0.13/0.44 -(iplus2 = iminus6) % 0.13/0.44 -(iplus2 = iplus5) % 0.13/0.44 -(iplus2 = iminus2) % 0.13/0.44 -(iplus2 = iminus8) % 0.13/0.44 -(iplus2 = iplus9) % 0.13/0.44 -(iplus2 = iF) % 0.13/0.44 -(iminus2 = iminus3) % 0.13/0.44 -(iminus2 = iminus1) % 0.13/0.44 -(iminus2 = iplus4) % 0.13/0.44 -(iminus2 = iplus7) % 0.13/0.44 -(iminus2 = iplus6) % 0.13/0.44 -(iminus2 = iminus5) % 0.13/0.44 -(iminus2 = iplus2) % 0.13/0.44 -(iminus2 = iplus8) % 0.13/0.44 -(iminus2 = iminus9) % 0.13/0.44 -(iminus2 = iT) % 0.13/0.44 -(iplus8 = iplus3) % 0.13/0.44 -(iplus8 = iplus1) % 0.13/0.44 -(iplus8 = iminus4) % 0.13/0.44 -(iplus8 = iminus7) % 0.13/0.44 -(iplus8 = iminus6) % 0.13/0.44 -(iplus8 = iplus5) % 0.13/0.44 -(iplus8 = iminus2) % 0.13/0.44 -(iplus8 = iminus8) % 0.13/0.44 -(iplus8 = iplus9) % 0.13/0.44 -(iplus8 = iF) % 0.13/0.44 -(iminus8 = iminus3) % 0.13/0.44 -(iminus8 = iminus1) % 0.13/0.44 -(iminus8 = iplus4) % 0.13/0.44 -(iminus8 = iplus7) % 0.13/0.44 -(iminus8 = iplus6) % 0.13/0.44 -(iminus8 = iminus5) % 0.13/0.44 -(iminus8 = iplus2) % 0.13/0.44 -(iminus8 = iplus8) % 0.13/0.44 -(iminus8 = iminus9) % 0.13/0.44 -(iminus8 = iT) % 0.13/0.44 -(iplus9 = iminus3) % 0.13/0.44 -(iplus9 = iminus1) % 0.13/0.44 -(iplus9 = iplus4) % 0.13/0.44 -(iplus9 = iplus7) % 0.13/0.44 -(iplus9 = iplus6) % 0.13/0.44 -(iplus9 = iminus5) % 0.13/0.44 -(iplus9 = iplus2) % 0.13/0.44 -(iplus9 = iplus8) % 0.13/0.44 -(iplus9 = iminus9) % 0.13/0.44 -(iplus9 = iT) % 0.13/0.44 -(iminus9 = iplus3) % 0.13/0.44 -(iminus9 = iplus1) % 0.13/0.44 -(iminus9 = iminus4) % 0.13/0.44 -(iminus9 = iminus7) % 0.13/0.44 -(iminus9 = iminus6) % 0.13/0.44 -(iminus9 = iplus5) % 0.13/0.44 -(iminus9 = iminus2) % 0.13/0.44 -(iminus9 = iminus8) % 0.13/0.44 -(iminus9 = iplus9) % 0.13/0.44 -(iminus9 = iF) % 0.13/0.44 -(iF = iminus3) % 0.13/0.44 -(iF = iminus1) % 0.13/0.44 -(iF = iplus4) % 0.13/0.44 -(iF = iplus7) % 0.13/0.44 -(iF = iplus6) % 0.13/0.44 -(iF = iminus5) % 0.13/0.44 -(iF = iplus2) % 0.13/0.44 -(iF = iplus8) % 0.13/0.44 -(iF = iminus9) % 0.13/0.44 -(iF = iT) % 0.13/0.44 -(iT = iplus3) % 0.13/0.44 -(iT = iplus1) % 0.13/0.44 -(iT = iminus4) % 0.13/0.44 -(iT = iminus7) % 0.13/0.44 -(iT = iminus6) % 0.13/0.44 -(iT = iplus5) % 0.13/0.44 -(iT = iminus2) % 0.13/0.44 -(iT = iminus8) % 0.13/0.44 -(iT = iplus9) % 0.13/0.44 -(iT = iF) % 0.13/0.44 +cTorF(iminus3) % 0.13/0.44 +cTorF(iplus3) % 0.13/0.44 +cTorF(iminus1) % 0.13/0.44 +cTorF(iplus1) % 0.13/0.44 +cTorF(iplus4) % 0.13/0.44 +cTorF(iminus4) % 0.13/0.44 +cTorF(iplus7) % 0.13/0.44 +cTorF(iminus7) % 0.13/0.44 +cTorF(iplus6) % 0.13/0.44 +cTorF(iminus6) % 0.13/0.44 +cTorF(iminus5) % 0.13/0.44 +cTorF(iplus5) % 0.13/0.44 +cTorF(iplus2) % 0.13/0.44 +cTorF(iminus2) % 0.13/0.44 +cTorF(iplus8) % 0.13/0.44 +cTorF(iminus8) % 0.13/0.44 +cTorF(iplus9) % 0.13/0.44 +cTorF(iminus9) % 0.13/0.44 +cTorF(iF) % 0.13/0.44 +cTorF(iT) % 0.13/0.44 -cowlNothing(_0) % 0.13/0.44 +xsd_integer(=0) % 0.13/0.44 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------