%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN514-1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n016.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 : Thu Jul 21 03:50:57 EDT 2022 % Result : Satisfiable 0.21s 0.41s % Output : Model 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SYN514-1 : TPTP v8.1.0. Released v2.1.0. % 0.07/0.13 % Command : darwin -pl 0 -pmc true -to %d %s % 0.13/0.35 % Computer : n016.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 % DateTime : Mon Jul 11 14:49:43 EDT 2022 % 0.13/0.35 % CPUTime : % 0.13/0.36 Defaulting to tptp format. % 0.21/0.41 SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.41 % 0.21/0.41 MODEL (CONTEXT): % 0.21/0.41 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.41 -__-v__(=0) % 0.21/0.41 +__con141 % 0.21/0.41 +__con142 % 0.21/0.41 +__con147 % 0.21/0.41 -__con148 % 0.21/0.41 +__con149 % 0.21/0.41 -__con158 % 0.21/0.41 +__con159 % 0.21/0.41 +__con160 % 0.21/0.41 +__con170 % 0.21/0.41 -__con171 % 0.21/0.41 +__con172 % 0.21/0.41 +__con173 % 0.21/0.41 +__con175 % 0.21/0.41 +__con182 % 0.21/0.41 +__con186 % 0.21/0.41 +c1_0 % 0.21/0.41 -c1_1(a263) % 0.21/0.41 -c1_1(a201) % 0.21/0.41 -c1_1(a191) % 0.21/0.41 -c1_1(a186) % 0.21/0.41 -c1_1(a259) % 0.21/0.41 -c1_1(a199) % 0.21/0.41 +c1_2(a207, a222) % 0.21/0.41 +c1_2(a207, a184) % 0.21/0.41 +c1_2(a207, a190) % 0.21/0.41 +c1_2(a263, a264) % 0.21/0.41 +c1_2(a186, a187) % 0.21/0.41 -c1_2(a214, a215) % 0.21/0.41 -c2_0 % 0.21/0.41 +c2_1(a188) % 0.21/0.41 +c2_1(a201) % 0.21/0.41 +c2_1(a193) % 0.21/0.41 +c2_1(a192) % 0.21/0.41 +c2_1(a191) % 0.21/0.41 -c2_1(a207) % 0.21/0.41 +c2_2(a207, a216) % 0.21/0.41 +c2_2(a207, a190) % 0.21/0.41 +c2_2(a214, a216) % 0.21/0.41 +c2_2(a189, a216) % 0.21/0.41 +c2_2(a255, a216) % 0.21/0.41 +c2_2(a209, a210) % 0.21/0.41 -c2_2(a207, a222) % 0.21/0.41 -c2_2(a186, a187) % 0.21/0.41 -c3_0 % 0.21/0.41 +c3_1(=0) % 0.21/0.41 +c3_1(a202) % 0.21/0.41 +c3_1(a188) % 0.21/0.41 +c3_1(a193) % 0.21/0.41 +c3_1(a209) % 0.21/0.41 -c3_1(a207) % 0.21/0.41 -c3_1(a214) % 0.21/0.41 -c3_1(a189) % 0.21/0.41 -c3_1(a255) % 0.21/0.41 +c3_2(a207, a184) % 0.21/0.41 +c3_2(a263, a264) % 0.21/0.41 -c3_2(a207, a208) % 0.21/0.41 -c3_2(a207, a216) % 0.21/0.41 -c3_2(a214, a216) % 0.21/0.41 -c3_2(a214, a215) % 0.21/0.41 -c3_2(a189, a216) % 0.21/0.41 -c3_2(a186, a187) % 0.21/0.41 -c3_2(a255, a216) % 0.21/0.41 -c3_2(a209, a210) % 0.21/0.41 -c4_0 % 0.21/0.41 +c4_1(a207) % 0.21/0.41 +c4_1(a188) % 0.21/0.41 +c4_1(a193) % 0.21/0.41 -c4_1(a192) % 0.21/0.41 -c4_1(a209) % 0.21/0.41 -c4_1(a199) % 0.21/0.41 +c4_2(a207, a208) % 0.21/0.41 -c4_2(a263, a264) % 0.21/0.41 -c4_2(a214, a216) % 0.21/0.41 -c5_0 % 0.21/0.41 +c5_1(a207) % 0.21/0.41 +c5_1(a188) % 0.21/0.41 +c5_1(a193) % 0.21/0.41 -c5_1(a192) % 0.21/0.41 -c5_1(a209) % 0.21/0.41 -c5_1(a199) % 0.21/0.41 +c5_2(a207, a208) % 0.21/0.41 -c5_2(a214, a215) % 0.21/0.41 +ndr1_0 % 0.21/0.41 +ndr1_1(=0) % 0.21/0.41 +ndr1_1(a207) % 0.21/0.41 +ndr1_1(a263) % 0.21/0.41 +ndr1_1(a214) % 0.21/0.41 +ndr1_1(a189) % 0.21/0.41 +ndr1_1(a186) % 0.21/0.41 +ndr1_1(a255) % 0.21/0.41 +ndr1_1(a209) % 0.21/0.41 -ndr1_1(a188) % 0.21/0.41 -ndr1_1(a193) % 0.21/0.41 +ssSkC0 % 0.21/0.41 +ssSkC1 % 0.21/0.41 +ssSkC10 % 0.21/0.41 +ssSkC11 % 0.21/0.41 +ssSkC12 % 0.21/0.41 +ssSkC13 % 0.21/0.41 +ssSkC14 % 0.21/0.41 +ssSkC15 % 0.21/0.41 +ssSkC16 % 0.21/0.41 +ssSkC2 % 0.21/0.41 +ssSkC3 % 0.21/0.41 +ssSkC4 % 0.21/0.41 +ssSkC5 % 0.21/0.41 +ssSkC7 % 0.21/0.41 +ssSkP0(=0) % 0.21/0.41 +ssSkP0(a188) % 0.21/0.41 +ssSkP0(a193) % 0.21/0.41 +ssSkP1(=0) % 0.21/0.41 +ssSkP1(a188) % 0.21/0.41 +ssSkP1(a193) % 0.21/0.41 +ssSkP2(=0) % 0.21/0.41 +ssSkP2(a188) % 0.21/0.41 +ssSkP2(a193) % 0.21/0.41 -ssSkP2(a207) % 0.21/0.41 -ssSkP2(a214) % 0.21/0.41 -ssSkP2(a189) % 0.21/0.41 -ssSkP2(a255) % 0.21/0.41 +ssSkP3(=0) % 0.21/0.41 +ssSkP3(a188) % 0.21/0.41 +ssSkP3(a193) % 0.21/0.41 -ssSkP3(a207) % 0.21/0.41 +ssSkP4(=0) % 0.21/0.41 +ssSkP4(a188) % 0.21/0.41 +ssSkP4(a193) % 0.21/0.41 +ssSkP5(=0) % 0.21/0.41 +ssSkP5(a188) % 0.21/0.41 +ssSkP5(a193) % 0.21/0.41 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------