↑ Up

Darwin---1.4.5.SAT-Mod.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Darwin---1.4.5
% Problem  : SYN423-1 : TPTP v8.1.0. Released v2.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : darwin -pl 0 -pmc true -to %d %s

% Computer : n010.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:49:50 EDT 2022

% Result   : Satisfiable 0.22s 0.45s
% Output   : Model 0.22s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14  % Problem  : SYN423-1 : TPTP v8.1.0. Released v2.1.0.
% 0.13/0.14  % Command  : darwin -pl 0 -pmc true -to %d %s
% 0.14/0.36  % Computer : n010.cluster.edu
% 0.14/0.36  % Model    : x86_64 x86_64
% 0.14/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36  % Memory   : 8042.1875MB
% 0.14/0.36  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36  % CPULimit : 300
% 0.14/0.36  % DateTime : Tue Jul 12 05:24:45 EDT 2022
% 0.14/0.36  % CPUTime  : 
% 0.14/0.37  Defaulting to tptp format.
% 0.22/0.45  SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/0.45  
% 0.22/0.45  MODEL (CONTEXT):
% 0.22/0.45  SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/0.45  -__-v__(=0)
% 0.22/0.45  +__con285
% 0.22/0.45  +__con286
% 0.22/0.45  -__con287
% 0.22/0.45  -__con288
% 0.22/0.45  +__con289
% 0.22/0.45  +__con295
% 0.22/0.45  +__con296
% 0.22/0.45  +__con301
% 0.22/0.45  +__con302
% 0.22/0.45  -__con303
% 0.22/0.45  +__con304
% 0.22/0.45  -__con305
% 0.22/0.45  +__con306
% 0.22/0.45  +__con313
% 0.22/0.45  +__con316
% 0.22/0.45  +__con317
% 0.22/0.45  +__con318
% 0.22/0.45  -c10_0
% 0.22/0.45  +c10_1(a564)
% 0.22/0.45  +c10_1(a528)
% 0.22/0.45  +c10_1(a474)
% 0.22/0.45  +c10_1(a553)
% 0.22/0.45  +c10_1(a514)
% 0.22/0.45  -c10_1(a574)
% 0.22/0.45  -c10_1(a542)
% 0.22/0.45  +c10_2(a615, a597)
% 0.22/0.45  +c10_2(a516, a597)
% 0.22/0.45  +c10_2(a457, a459)
% 0.22/0.45  +c10_2(a564, a565)
% 0.22/0.45  +c10_2(a528, a442)
% 0.22/0.45  +c10_2(a568, a569)
% 0.22/0.45  +c10_2(a553, a442)
% 0.22/0.45  +c10_2(a562, a597)
% 0.22/0.45  -c10_2(a572, a573)
% 0.22/0.45  -c10_2(a443, a445)
% 0.22/0.45  +c1_0
% 0.22/0.45  +c1_1(a516)
% 0.22/0.45  +c1_1(a574)
% 0.22/0.45  -c1_1(a615)
% 0.22/0.45  -c1_1(a572)
% 0.22/0.45  -c1_1(a564)
% 0.22/0.45  -c1_1(a544)
% 0.22/0.45  -c1_1(a588)
% 0.22/0.45  +c1_2(a611, a612)
% 0.22/0.45  +c1_2(a457, a458)
% 0.22/0.45  +c1_2(a443, a444)
% 0.22/0.45  +c1_2(a553, a551)
% 0.22/0.45  +c1_2(a553, a554)
% 0.22/0.45  -c1_2(a572, a573)
% 0.22/0.45  -c1_2(a588, a589)
% 0.22/0.45  +c2_0
% 0.22/0.45  +c2_1(a516)
% 0.22/0.45  +c2_1(a544)
% 0.22/0.45  +c2_1(a553)
% 0.22/0.45  +c2_2(a553, a551)
% 0.22/0.45  +c2_2(a553, a554)
% 0.22/0.45  -c2_2(a508, a509)
% 0.22/0.45  -c2_2(a457, a459)
% 0.22/0.45  -c2_2(a455, a456)
% 0.22/0.45  -c2_2(a453, a454)
% 0.22/0.45  +c3_0
% 0.22/0.45  +c3_1(a553)
% 0.22/0.45  -c3_1(a516)
% 0.22/0.45  -c3_1(a619)
% 0.22/0.45  -c3_1(a574)
% 0.22/0.45  -c3_1(a544)
% 0.22/0.45  -c3_1(a588)
% 0.22/0.45  +c3_2(a568, a569)
% 0.22/0.45  -c3_2(a615, a597)
% 0.22/0.45  -c3_2(a516, a597)
% 0.22/0.45  -c3_2(a553, a554)
% 0.22/0.45  -c3_2(a588, a589)
% 0.22/0.45  -c3_2(a562, a597)
% 0.22/0.45  -c4_0
% 0.22/0.45  +c4_1(a558)
% 0.22/0.45  +c4_1(a443)
% 0.22/0.45  -c4_1(a516)
% 0.22/0.45  +c4_2(a564, a565)
% 0.22/0.45  +c4_2(a528, a529)
% 0.22/0.45  -c4_2(a457, a459)
% 0.22/0.45  -c4_2(a455, a456)
% 0.22/0.45  -c4_2(a443, a444)
% 0.22/0.45  -c4_2(a553, a439)
% 0.22/0.45  +c5_0
% 0.22/0.45  +c5_1(a528)
% 0.22/0.45  +c5_1(a553)
% 0.22/0.45  -c5_1(a544)
% 0.22/0.45  -c5_1(a575)
% 0.22/0.45  +c5_2(a528, a442)
% 0.22/0.45  +c5_2(a451, a452)
% 0.22/0.45  +c5_2(a568, a570)
% 0.22/0.45  +c5_2(a443, a445)
% 0.22/0.45  +c5_2(a553, a442)
% 0.22/0.45  -c5_2(a615, a597)
% 0.22/0.45  -c5_2(a611, a612)
% 0.22/0.45  -c5_2(a516, a597)
% 0.22/0.45  -c5_2(a508, a509)
% 0.22/0.45  -c5_2(a453, a454)
% 0.22/0.45  -c5_2(a553, a439)
% 0.22/0.45  -c5_2(a562, a597)
% 0.22/0.45  +c6_0
% 0.22/0.45  +c6_1(a611)
% 0.22/0.45  +c6_1(a564)
% 0.22/0.45  +c6_1(a528)
% 0.22/0.45  +c6_1(a544)
% 0.22/0.45  -c6_1(a451)
% 0.22/0.45  +c6_2(a588, a589)
% 0.22/0.45  -c6_2(a451, a452)
% 0.22/0.45  -c6_2(a553, a439)
% 0.22/0.45  +c7_0
% 0.22/0.45  +c7_1(a615)
% 0.22/0.45  +c7_1(a516)
% 0.22/0.45  +c7_1(a562)
% 0.22/0.45  -c7_1(a568)
% 0.22/0.45  -c7_1(a544)
% 0.22/0.45  -c7_1(a575)
% 0.22/0.45  +c7_2(a470, a471)
% 0.22/0.45  +c7_2(a453, a454)
% 0.22/0.45  +c7_2(a528, a529)
% 0.22/0.45  -c7_2(a611, a612)
% 0.22/0.45  -c7_2(a528, a442)
% 0.22/0.45  -c7_2(a568, a570)
% 0.22/0.45  -c7_2(a553, a551)
% 0.22/0.45  -c7_2(a553, a442)
% 0.22/0.45  -c8_0
% 0.22/0.45  +c8_1(a470)
% 0.22/0.45  +c8_1(a453)
% 0.22/0.45  +c8_1(a619)
% 0.22/0.45  -c8_1(a474)
% 0.22/0.45  +c8_2(a572, a573)
% 0.22/0.45  +c8_2(a470, a471)
% 0.22/0.45  +c8_2(a455, a456)
% 0.22/0.45  +c8_2(a568, a570)
% 0.22/0.45  -c8_2(a457, a458)
% 0.22/0.45  -c8_2(a443, a445)
% 0.22/0.45  +c9_0
% 0.22/0.45  +c9_1(a516)
% 0.22/0.45  +c9_1(a544)
% 0.22/0.45  -c9_1(a558)
% 0.22/0.45  -c9_1(a448)
% 0.22/0.45  -c9_1(a553)
% 0.22/0.45  +c9_2(a528, a529)
% 0.22/0.45  +c9_2(a568, a569)
% 0.22/0.45  -c9_2(a508, a509)
% 0.22/0.45  -c9_2(a451, a452)
% 0.22/0.45  +ndr1_0
% 0.22/0.45  +ndr1_1(=0)
% 0.22/0.45  +ndr1_1(a615)
% 0.22/0.45  +ndr1_1(a611)
% 0.22/0.45  +ndr1_1(a572)
% 0.22/0.45  +ndr1_1(a516)
% 0.22/0.45  +ndr1_1(a508)
% 0.22/0.45  +ndr1_1(a470)
% 0.22/0.45  +ndr1_1(a457)
% 0.22/0.45  +ndr1_1(a455)
% 0.22/0.45  +ndr1_1(a453)
% 0.22/0.45  +ndr1_1(a564)
% 0.22/0.45  +ndr1_1(a528)
% 0.22/0.45  +ndr1_1(a451)
% 0.22/0.45  +ndr1_1(a568)
% 0.22/0.45  +ndr1_1(a443)
% 0.22/0.45  +ndr1_1(a553)
% 0.22/0.45  +ndr1_1(a588)
% 0.22/0.45  +ndr1_1(a562)
% 0.22/0.45  -ndr1_1(a544)
% 0.22/0.45  -ndr1_1(a575)
% 0.22/0.45  +ssSkC0
% 0.22/0.45  +ssSkC1
% 0.22/0.45  +ssSkC10
% 0.22/0.45  +ssSkC12
% 0.22/0.45  +ssSkC14
% 0.22/0.45  +ssSkC16
% 0.22/0.45  +ssSkC18
% 0.22/0.45  +ssSkC2
% 0.22/0.45  +ssSkC21
% 0.22/0.45  +ssSkC22
% 0.22/0.45  +ssSkC23
% 0.22/0.45  +ssSkC24
% 0.22/0.45  +ssSkC25
% 0.22/0.45  +ssSkC26
% 0.22/0.45  +ssSkC27
% 0.22/0.45  +ssSkC29
% 0.22/0.45  +ssSkC3
% 0.22/0.45  +ssSkC31
% 0.22/0.45  +ssSkC32
% 0.22/0.45  +ssSkC33
% 0.22/0.45  +ssSkC34
% 0.22/0.45  +ssSkC37
% 0.22/0.45  +ssSkC38
% 0.22/0.45  +ssSkC39
% 0.22/0.45  +ssSkC4
% 0.22/0.45  +ssSkC40
% 0.22/0.45  +ssSkC41
% 0.22/0.45  +ssSkC6
% 0.22/0.45  +ssSkC7
% 0.22/0.45  +ssSkC8
% 0.22/0.45  +ssSkC9
% 0.22/0.45  +ssSkP0(=0)
% 0.22/0.45  +ssSkP0(a544)
% 0.22/0.45  +ssSkP0(a575)
% 0.22/0.45  +ssSkP1(=0)
% 0.22/0.45  +ssSkP1(a544)
% 0.22/0.45  +ssSkP1(a575)
% 0.22/0.45  +ssSkP10(=0)
% 0.22/0.45  +ssSkP10(a544)
% 0.22/0.45  +ssSkP10(a575)
% 0.22/0.45  +ssSkP11(=0)
% 0.22/0.45  +ssSkP11(a544)
% 0.22/0.45  +ssSkP11(a575)
% 0.22/0.45  +ssSkP2(=0)
% 0.22/0.45  +ssSkP2(a544)
% 0.22/0.45  +ssSkP2(a575)
% 0.22/0.45  +ssSkP3(=0)
% 0.22/0.45  +ssSkP3(a544)
% 0.22/0.45  +ssSkP3(a575)
% 0.22/0.45  +ssSkP4(=0)
% 0.22/0.45  +ssSkP4(a544)
% 0.22/0.45  +ssSkP4(a575)
% 0.22/0.45  +ssSkP5(=0)
% 0.22/0.45  +ssSkP5(a544)
% 0.22/0.45  +ssSkP5(a575)
% 0.22/0.45  +ssSkP6(=0)
% 0.22/0.45  +ssSkP6(a544)
% 0.22/0.45  +ssSkP6(a575)
% 0.22/0.45  +ssSkP7(=0)
% 0.22/0.45  +ssSkP7(a544)
% 0.22/0.45  +ssSkP7(a575)
% 0.22/0.45  -ssSkP7(a553)
% 0.22/0.45  +ssSkP8(=0)
% 0.22/0.45  +ssSkP8(a544)
% 0.22/0.45  +ssSkP8(a575)
% 0.22/0.45  +ssSkP9(=0)
% 0.22/0.45  +ssSkP9(a544)
% 0.22/0.45  +ssSkP9(a575)
% 0.22/0.45  SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------