↑ Up

Darwin---1.4.5.CSA-Mod.s

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

% Computer : n027.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:54 EDT 2022

% Result   : CounterSatisfiable 1.45s 1.68s
% Output   : Model 1.45s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SYN427+1 : TPTP v8.1.0. Released v2.1.0.
% 0.07/0.13  % Command  : darwin -pl 0 -pmc true -to %d %s
% 0.12/0.34  % Computer : n027.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  % DateTime : Mon Jul 11 22:13:34 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 0.12/0.34  Defaulting to tptp format.
% 1.45/1.68  SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.45/1.68  
% 1.45/1.68  MODEL (CONTEXT):
% 1.45/1.68  SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.45/1.68  -__-v__(=0)
% 1.45/1.68  -__con314
% 1.45/1.68  +__con316
% 1.45/1.68  -__con317
% 1.45/1.68  -__con321
% 1.45/1.68  -__con323
% 1.45/1.68  +__con324
% 1.45/1.68  -__con327
% 1.45/1.68  -__con328
% 1.45/1.68  -__con329
% 1.45/1.68  -__con330
% 1.45/1.68  +__con333
% 1.45/1.68  -__con335
% 1.45/1.68  -__con336
% 1.45/1.68  +__con345
% 1.45/1.68  +__con346
% 1.45/1.68  +__con357
% 1.45/1.68  +__con358
% 1.45/1.68  +__con364
% 1.45/1.68  +__con365
% 1.45/1.68  +__con366
% 1.45/1.68  +__con367
% 1.45/1.68  +__con368
% 1.45/1.68  +__con369
% 1.45/1.68  -__con382
% 1.45/1.68  -__con384
% 1.45/1.68  -__con386
% 1.45/1.68  +__con392
% 1.45/1.68  +__con394
% 1.45/1.68  -__con398
% 1.45/1.68  +__con399
% 1.45/1.68  -__con400
% 1.45/1.68  +__con403
% 1.45/1.68  +__con409
% 1.45/1.68  -__con412
% 1.45/1.68  -__con413
% 1.45/1.68  +__con414
% 1.45/1.68  +__con423
% 1.45/1.68  +__con424
% 1.45/1.68  +__con425
% 1.45/1.68  -__con427
% 1.45/1.68  -__con437
% 1.45/1.68  -__con439
% 1.45/1.68  +__con444
% 1.45/1.68  +__con445
% 1.45/1.68  -__con446
% 1.45/1.68  +__con447
% 1.45/1.68  -__con448
% 1.45/1.68  -__con449
% 1.45/1.68  -__con450
% 1.45/1.68  -__con451
% 1.45/1.68  -__con452
% 1.45/1.68  +__con454
% 1.45/1.68  +__con455
% 1.45/1.68  +__con456
% 1.45/1.68  +__con457
% 1.45/1.68  +__con458
% 1.45/1.68  +__con459
% 1.45/1.68  +__con460
% 1.45/1.68  +__con461
% 1.45/1.68  -__con465
% 1.45/1.68  -__con466
% 1.45/1.68  -__con468
% 1.45/1.68  -__con469
% 1.45/1.68  -__con470
% 1.45/1.68  -__con471
% 1.45/1.68  +__con472
% 1.45/1.68  -__con473
% 1.45/1.68  +__con474
% 1.45/1.68  -__con475
% 1.45/1.68  -__con476
% 1.45/1.68  +__con479
% 1.45/1.68  +__con480
% 1.45/1.68  +__con481
% 1.45/1.68  -__con482
% 1.45/1.68  +__con483
% 1.45/1.68  +__con484
% 1.45/1.68  +__con496
% 1.45/1.68  +__con497
% 1.45/1.68  +__con498
% 1.45/1.68  +__con503
% 1.45/1.68  +__con506
% 1.45/1.68  +__con511
% 1.45/1.68  +__con512
% 1.45/1.68  +__con513
% 1.45/1.68  +__con514
% 1.45/1.68  +__con515
% 1.45/1.68  +__con516
% 1.45/1.68  +__con517
% 1.45/1.68  +__con518
% 1.45/1.68  +__con531
% 1.45/1.68  +__con532
% 1.45/1.68  -__con533
% 1.45/1.68  -__con536
% 1.45/1.68  +__con537
% 1.45/1.68  +__con538
% 1.45/1.68  -__con539
% 1.45/1.68  +__con548
% 1.45/1.68  +__con549
% 1.45/1.68  +__con550
% 1.45/1.68  +__con551
% 1.45/1.68  +__con552
% 1.45/1.68  +__con553
% 1.45/1.69  +__con554
% 1.45/1.69  +__con555
% 1.45/1.69  +__con556
% 1.45/1.69  +__con560
% 1.45/1.69  -__con561
% 1.45/1.69  -__con562
% 1.45/1.69  -__con566
% 1.45/1.69  +__con568
% 1.45/1.69  +__con575
% 1.45/1.69  -__con583
% 1.45/1.69  -__con584
% 1.45/1.69  -__con585
% 1.45/1.69  -__con587
% 1.45/1.69  +__con588
% 1.45/1.69  -__con595
% 1.45/1.69  -__con596
% 1.45/1.69  -__con597
% 1.45/1.69  +__con604
% 1.45/1.69  -__con605
% 1.45/1.69  +__con608
% 1.45/1.69  +__con609
% 1.45/1.69  -__con614
% 1.45/1.69  -__con615
% 1.45/1.69  -__con616
% 1.45/1.69  -__con618
% 1.45/1.69  -__con619
% 1.45/1.69  -__con620
% 1.45/1.69  -__con630
% 1.45/1.69  -__con631
% 1.45/1.69  -__con632
% 1.45/1.69  +__con633
% 1.45/1.69  -__con634
% 1.45/1.69  -__con635
% 1.45/1.69  -__con636
% 1.45/1.69  -__con641
% 1.45/1.69  -__con642
% 1.45/1.69  +__con643
% 1.45/1.69  -__con644
% 1.45/1.69  +__con645
% 1.45/1.69  +__con646
% 1.45/1.69  -__con649
% 1.45/1.69  -__con650
% 1.45/1.69  +__con657
% 1.45/1.69  -__con663
% 1.45/1.69  +__con664
% 1.45/1.69  -__con665
% 1.45/1.69  +__con666
% 1.45/1.69  +__con667
% 1.45/1.69  -__con670
% 1.45/1.69  +__con671
% 1.45/1.69  +__con672
% 1.45/1.69  +__con673
% 1.45/1.69  +__con674
% 1.45/1.69  -__con676
% 1.45/1.69  -__con677
% 1.45/1.69  +c10_0
% 1.45/1.69  +c10_1(a1611)
% 1.45/1.69  +c10_1(a1620)
% 1.45/1.69  +c10_1(a1677)
% 1.45/1.69  +c10_1(a1817)
% 1.45/1.69  +c10_2(a1683, a1676)
% 1.45/1.69  +c10_2(a1702, a1703)
% 1.45/1.69  +c10_2(a1795, a1797)
% 1.45/1.69  +c10_2(a1798, a1799)
% 1.45/1.69  +c1_0
% 1.45/1.69  +c1_1(a1601)
% 1.45/1.69  +c1_1(a1620)
% 1.45/1.69  +c1_1(a1629)
% 1.45/1.69  +c1_1(a1677)
% 1.45/1.69  +c1_1(a1679)
% 1.45/1.69  +c1_1(a1681)
% 1.45/1.69  +c1_1(a1711)
% 1.45/1.69  +c1_1(a1802)
% 1.45/1.69  -c1_1(a1705)
% 1.45/1.69  +c1_2(a1745, a1746)
% 1.45/1.69  +c2_0
% 1.45/1.69  +c2_1(a1587)
% 1.45/1.69  +c2_1(a1593)
% 1.45/1.69  +c2_1(a1601)
% 1.45/1.69  +c2_1(a1694)
% 1.45/1.69  +c2_1(a1702)
% 1.45/1.69  +c2_1(a1711)
% 1.45/1.69  +c2_1(a1736)
% 1.45/1.69  +c2_1(a1740)
% 1.45/1.69  +c2_1(a1767)
% 1.45/1.69  -c2_1(a1683)
% 1.45/1.69  +c2_2(a1620, a1810)
% 1.45/1.69  +c2_2(a1677, a1810)
% 1.45/1.69  +c2_2(a1679, =0)
% 1.45/1.69  +c2_2(a1681, a1810)
% 1.45/1.69  +c2_2(a1767, a1800)
% 1.45/1.69  -c2_2(a1679, a1658)
% 1.45/1.69  +c3_0
% 1.45/1.69  +c3_1(a1620)
% 1.45/1.69  +c3_1(a1677)
% 1.45/1.69  +c3_1(a1681)
% 1.45/1.69  -c3_1(a1705)
% 1.45/1.69  +c3_2(a1659, a1660)
% 1.45/1.69  +c3_2(a1679, a1658)
% 1.45/1.69  +c3_2(a1705, a1658)
% 1.45/1.69  -c4_0
% 1.45/1.69  +c4_1(=0)
% 1.45/1.69  +c4_1(a1667)
% 1.45/1.69  +c4_1(a1679)
% 1.45/1.69  +c4_1(a1802)
% 1.45/1.69  -c4_1(a1611)
% 1.45/1.69  -c4_1(a1620)
% 1.45/1.69  -c4_1(a1647)
% 1.45/1.69  -c4_1(a1677)
% 1.45/1.69  -c4_1(a1817)
% 1.45/1.69  +c4_2(a1631, a1633)
% 1.45/1.69  +c4_2(a1647, =0)
% 1.45/1.69  +c4_2(a1659, a1660)
% 1.45/1.69  +c4_2(a1659, a1661)
% 1.45/1.69  +c4_2(a1802, a1803)
% 1.45/1.69  +c4_2(a1817, a1818)
% 1.45/1.69  -c4_2(a1679, a1680)
% 1.45/1.69  +c5_0
% 1.45/1.69  +c5_1(a1618)
% 1.45/1.69  +c5_1(a1631)
% 1.45/1.69  +c5_1(a1683)
% 1.45/1.69  -c5_1(a1767)
% 1.45/1.69  +c5_2(a1659, a1660)
% 1.45/1.69  +c5_2(a1679, a1658)
% 1.45/1.69  +c5_2(a1683, a1684)
% 1.45/1.69  +c5_2(a1798, a1799)
% 1.45/1.69  +c5_2(a1802, a1804)
% 1.45/1.69  -c5_2(a1702, a1703)
% 1.45/1.69  +c6_0
% 1.45/1.69  +c6_1(a1736)
% 1.45/1.69  +c6_2(a1802, a1804)
% 1.45/1.69  -c6_2(a1683, a1684)
% 1.45/1.69  +c7_0
% 1.45/1.69  +c7_1(a1610)
% 1.45/1.69  +c7_1(a1802)
% 1.45/1.69  -c7_1(a1620)
% 1.45/1.69  -c7_1(a1677)
% 1.45/1.69  -c7_1(a1767)
% 1.45/1.69  +c7_2(a1620, a1621)
% 1.45/1.69  +c7_2(a1620, a1751)
% 1.45/1.69  +c7_2(a1677, a1751)
% 1.45/1.69  +c7_2(a1679, a1680)
% 1.45/1.69  +c7_2(a1681, a1751)
% 1.45/1.69  +c7_2(a1802, a1803)
% 1.45/1.69  -c8_0
% 1.45/1.69  +c8_1(a1611)
% 1.45/1.69  +c8_1(a1620)
% 1.45/1.69  +c8_1(a1647)
% 1.45/1.69  +c8_1(a1677)
% 1.45/1.69  +c8_1(a1681)
% 1.45/1.69  +c8_1(a1683)
% 1.45/1.69  +c8_1(a1817)
% 1.45/1.69  +c8_2(a1679, a1680)
% 1.45/1.69  +c8_2(a1683, a1676)
% 1.45/1.69  +c8_2(a1817, a1818)
% 1.45/1.69  +c8_2(a1820, a1821)
% 1.45/1.69  -c8_2(a1683, a1684)
% 1.45/1.69  +c9_0
% 1.45/1.69  +c9_1(a1593)
% 1.45/1.69  +c9_1(a1601)
% 1.45/1.69  +c9_1(a1683)
% 1.45/1.69  +c9_1(a1694)
% 1.45/1.69  +c9_1(a1702)
% 1.45/1.69  +c9_1(a1711)
% 1.45/1.69  -c9_1(a1679)
% 1.45/1.69  -c9_1(a1705)
% 1.45/1.69  +c9_2(a1610, a1682)
% 1.45/1.69  +c9_2(a1631, a1632)
% 1.45/1.69  +c9_2(a1631, a1633)
% 1.45/1.69  +c9_2(a1659, a1661)
% 1.45/1.69  +c9_2(a1802, a1682)
% 1.45/1.69  +c9_2(a1802, a1803)
% 1.45/1.69  -c9_2(a1702, a1703)
% 1.45/1.69  +epred10_0
% 1.45/1.69  +epred11_0
% 1.45/1.69  +epred13_0
% 1.45/1.69  +epred15_0
% 1.45/1.69  +epred17_0
% 1.45/1.69  +epred1_0
% 1.45/1.69  +epred2_0
% 1.45/1.69  +epred3_0
% 1.45/1.69  +epred4_0
% 1.45/1.69  +epred5_0
% 1.45/1.69  +epred6_0
% 1.45/1.69  +epred8_0
% 1.45/1.69  +ndr1_0
% 1.45/1.69  +ndr1_1(_0)
% 1.45/1.69  +ndr1_1(a1679)
% 1.45/1.69  +ndr1_1(a1702)
% 1.45/1.69  SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------