%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : LCL647+1.005 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n009.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 14:31:25 EDT 2022 % Result : Unknown 1.40s 1.62s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : LCL647+1.005 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : sos-script %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jul 3 06:46:37 EDT 2022 % 0.12/0.34 % CPUTime : % 1.18/1.40 ----- Otter 3.2, August 2001 ----- % 1.18/1.40 The process was started by sandbox on n009.cluster.edu, % 1.18/1.40 Sun Jul 3 06:46:37 2022 % 1.18/1.40 The command was "./sos". The process ID is 10993. % 1.18/1.40 % 1.18/1.40 set(prolog_style_variables). % 1.18/1.40 set(auto). % 1.18/1.40 dependent: set(auto1). % 1.18/1.40 dependent: set(process_input). % 1.18/1.40 dependent: clear(print_kept). % 1.18/1.40 dependent: clear(print_new_demod). % 1.18/1.40 dependent: clear(print_back_demod). % 1.18/1.40 dependent: clear(print_back_sub). % 1.18/1.40 dependent: set(control_memory). % 1.18/1.40 dependent: assign(max_mem, 12000). % 1.18/1.40 dependent: assign(pick_given_ratio, 4). % 1.18/1.40 dependent: assign(stats_level, 1). % 1.18/1.40 dependent: assign(pick_semantic_ratio, 3). % 1.18/1.40 dependent: assign(sos_limit, 5000). % 1.18/1.40 dependent: assign(max_weight, 60). % 1.18/1.40 clear(print_given). % 1.18/1.40 % 1.18/1.40 formula_list(usable). % 1.18/1.40 % 1.18/1.40 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=7. % 1.18/1.40 % 1.18/1.40 This is a non-Horn set without equality. The strategy % 1.18/1.40 will be ordered hyper_res, ur_res, unit deletion, and % 1.18/1.40 factoring, with satellites in sos and nuclei in usable. % 1.18/1.40 % 1.18/1.40 dependent: set(hyper_res). % 1.18/1.40 dependent: set(factor). % 1.18/1.40 dependent: set(unit_deletion). % 1.18/1.40 % 1.18/1.40 ------------> process usable: % 1.18/1.40 747 back subsumes 447. % 1.18/1.40 747 back subsumes 441. % 1.18/1.40 747 back subsumes 387. % 1.18/1.40 747 back subsumes 381. % 1.18/1.40 747 back subsumes 299. % 1.18/1.40 747 back subsumes 293. % 1.18/1.40 749 back subsumes 710. % 1.18/1.40 749 back subsumes 709. % 1.18/1.40 749 back subsumes 692. % 1.18/1.40 749 back subsumes 691. % 1.18/1.40 749 back subsumes 674. % 1.18/1.40 749 back subsumes 673. % 1.18/1.40 751 back subsumes 448. % 1.18/1.40 751 back subsumes 442. % 1.18/1.40 751 back subsumes 388. % 1.18/1.40 751 back subsumes 382. % 1.18/1.40 751 back subsumes 300. % 1.18/1.40 751 back subsumes 294. % 1.18/1.40 760 back subsumes 759. % 1.18/1.40 763 back subsumes 757. % 1.18/1.40 763 back subsumes 754. % 1.18/1.40 763 back subsumes 450. % 1.18/1.40 763 back subsumes 444. % 1.18/1.40 763 back subsumes 390. % 1.18/1.40 763 back subsumes 384. % 1.18/1.40 763 back subsumes 302. % 1.18/1.40 763 back subsumes 296. % 1.18/1.40 766 back subsumes 451. % 1.18/1.40 766 back subsumes 445. % 1.18/1.40 766 back subsumes 391. % 1.18/1.40 766 back subsumes 385. % 1.18/1.40 766 back subsumes 303. % 1.18/1.40 766 back subsumes 297. % 1.18/1.40 769 back subsumes 762. % 1.18/1.40 770 back subsumes 768. % 1.18/1.40 770 back subsumes 452. % 1.18/1.40 770 back subsumes 446. % 1.18/1.40 770 back subsumes 392. % 1.18/1.40 770 back subsumes 386. % 1.18/1.40 770 back subsumes 304. % 1.18/1.40 770 back subsumes 298. % 1.18/1.40 774 back subsumes 619. % 1.18/1.40 774 back subsumes 613. % 1.18/1.40 774 back subsumes 607. % 1.18/1.40 774 back subsumes 601. % 1.18/1.40 774 back subsumes 595. % 1.18/1.40 774 back subsumes 589. % 1.18/1.40 774 back subsumes 583. % 1.18/1.40 774 back subsumes 577. % 1.18/1.40 775 back subsumes 706. % 1.18/1.40 775 back subsumes 703. % 1.18/1.40 775 back subsumes 700. % 1.18/1.40 775 back subsumes 697. % 1.18/1.40 776 back subsumes 738. % 1.18/1.40 776 back subsumes 737. % 1.18/1.40 776 back subsumes 736. % 1.18/1.40 776 back subsumes 735. % 1.18/1.40 776 back subsumes 734. % 1.18/1.40 776 back subsumes 733. % 1.18/1.40 778 back subsumes 620. % 1.18/1.40 778 back subsumes 614. % 1.18/1.40 778 back subsumes 608. % 1.18/1.40 778 back subsumes 602. % 1.18/1.40 778 back subsumes 596. % 1.18/1.40 778 back subsumes 590. % 1.18/1.40 778 back subsumes 584. % 1.18/1.40 778 back subsumes 578. % 1.18/1.40 787 back subsumes 786. % 1.18/1.40 790 back subsumes 784. % 1.18/1.40 790 back subsumes 781. % 1.18/1.40 790 back subsumes 622. % 1.18/1.40 790 back subsumes 616. % 1.18/1.40 790 back subsumes 610. % 1.18/1.40 790 back subsumes 604. % 1.18/1.40 790 back subsumes 598. % 1.18/1.40 790 back subsumes 592. % 1.18/1.40 790 back subsumes 586. % 1.18/1.40 790 back subsumes 580. % 1.18/1.40 791 back subsumes 708. % 1.18/1.40 791 back subsumes 705. % 1.18/1.40 791 back subsumes 702. % 1.18/1.40 791 back subsumes 699. % 1.18/1.40 793 back subsumes 623. % 1.18/1.40 793 back subsumes 617. % 1.18/1.40 793 back subsumes 611. % 1.18/1.40 793 back subsumes 605. % 1.18/1.40 793 back subsumes 599. % 1.18/1.40 793 back subsumes 593. % 1.18/1.40 793 back subsumes 587. % 1.18/1.40 793 back subsumes 581. % 1.18/1.40 796 back subsumes 789. % 1.18/1.40 797 back subsumes 795. % 1.18/1.40 797 back subsumes 624. % 1.18/1.40 797 back subsumes 618. % 1.18/1.40 797 back subsumes 612. % 1.18/1.40 797 back subsumes 606. % 1.18/1.40 797 back subsumes 600. % 1.18/1.40 797 back subsumes 594. % 1.18/1.40 797 back subsumes 588. % 1.18/1.40 797 back subsumes 582. % 1.18/1.40 801 back subsumes 459. % 1.18/1.40 801 back subsumes 453. % 1.18/1.40 801 back subsumes 399. % 1.18/1.40 801 back subsumes 393. % 1.18/1.40 801 back subsumes 311. % 1.18/1.40 801 back subsumes 305. % 1.18/1.40 802 back subsumes 628. % 1.18/1.40 802 back subsumes 625. % 1.18/1.40 802 back subsumes 568. % 1.18/1.40 802 back subsumes 565. % 1.18/1.40 802 back subsumes 520. % 1.18/1.40 802 back subsumes 517. % 1.18/1.40 803 back subsumes 712. % 1.18/1.40 803 back subsumes 711. % 1.18/1.40 803 back subsumes 694. % 1.18/1.40 803 back subsumes 693. % 1.18/1.40 803 back subsumes 676. % 1.18/1.40 803 back subsumes 675. % 1.18/1.40 805 back subsumes 460. % 1.18/1.40 805 back subsumes 454. % 1.18/1.40 805 back subsumes 400. % 1.18/1.40 805 back subsumes 394. % 1.18/1.40 805 back subsumes 312. % 1.18/1.40 805 back subsumes 306. % 1.18/1.40 814 back subsumes 813. % 1.18/1.40 817 back subsumes 811. % 1.18/1.40 817 back subsumes 808. % 1.18/1.40 817 back subsumes 462. % 1.18/1.40 817 back subsumes 456. % 1.18/1.40 817 back subsumes 402. % 1.40/1.61 817 back subsumes 396. % 1.40/1.61 817 back subsumes 314. % 1.40/1.61 817 back subsumes 308. % 1.40/1.61 818 back subsumes 630. % 1.40/1.61 818 back subsumes 627. % 1.40/1.61 818 back subsumes 570. % 1.40/1.61 818 back subsumes 567. % 1.40/1.61 818 back subsumes 522. % 1.40/1.61 818 back subsumes 519. % 1.40/1.61 820 back subsumes 463. % 1.40/1.61 820 back subsumes 457. % 1.40/1.61 820 back subsumes 403. % 1.40/1.61 820 back subsumes 397. % 1.40/1.61 820 back subsumes 315. % 1.40/1.61 820 back subsumes 309. % 1.40/1.61 823 back subsumes 816. % 1.40/1.61 824 back subsumes 822. % 1.40/1.61 824 back subsumes 464. % 1.40/1.61 824 back subsumes 458. % 1.40/1.61 824 back subsumes 404. % 1.40/1.61 824 back subsumes 398. % 1.40/1.61 824 back subsumes 316. % 1.40/1.61 824 back subsumes 310. % 1.40/1.61 828 back subsumes 471. % 1.40/1.61 828 back subsumes 465. % 1.40/1.61 828 back subsumes 411. % 1.40/1.61 828 back subsumes 405. % 1.40/1.61 828 back subsumes 323. % 1.40/1.61 828 back subsumes 317. % 1.40/1.61 829 back subsumes 634. % 1.40/1.61 829 back subsumes 631. % 1.40/1.61 829 back subsumes 574. % 1.40/1.61 829 back subsumes 571. % 1.40/1.61 829 back subsumes 526. % 1.40/1.61 829 back subsumes 523. % 1.40/1.61 830 back subsumes 714. % 1.40/1.61 830 back subsumes 713. % 1.40/1.61 830 back subsumes 696. % 1.40/1.61 830 back subsumes 695. % 1.40/1.61 830 back subsumes 678. % 1.40/1.61 830 back subsumes 677. % 1.40/1.61 832 back subsumes 472. % 1.40/1.61 832 back subsumes 466. % 1.40/1.61 832 back subsumes 412. % 1.40/1.61 832 back subsumes 406. % 1.40/1.61 832 back subsumes 324. % 1.40/1.61 832 back subsumes 318. % 1.40/1.61 841 back subsumes 840. % 1.40/1.61 844 back subsumes 838. % 1.40/1.61 844 back subsumes 835. % 1.40/1.61 844 back subsumes 474. % 1.40/1.61 844 back subsumes 468. % 1.40/1.61 844 back subsumes 414. % 1.40/1.61 844 back subsumes 408. % 1.40/1.61 844 back subsumes 326. % 1.40/1.61 844 back subsumes 320. % 1.40/1.61 845 back subsumes 636. % 1.40/1.61 845 back subsumes 633. % 1.40/1.61 845 back subsumes 576. % 1.40/1.61 845 back subsumes 573. % 1.40/1.61 845 back subsumes 528. % 1.40/1.61 845 back subsumes 525. % 1.40/1.61 847 back subsumes 475. % 1.40/1.61 847 back subsumes 469. % 1.40/1.61 847 back subsumes 415. % 1.40/1.61 847 back subsumes 409. % 1.40/1.61 847 back subsumes 327. % 1.40/1.61 847 back subsumes 321. % 1.40/1.61 850 back subsumes 843. % 1.40/1.61 851 back subsumes 849. % 1.40/1.61 851 back subsumes 476. % 1.40/1.61 851 back subsumes 470. % 1.40/1.61 851 back subsumes 416. % 1.40/1.61 851 back subsumes 410. % 1.40/1.61 851 back subsumes 328. % 1.40/1.61 851 back subsumes 322. % 1.40/1.61 % 1.40/1.61 ------------> process sos: % 1.40/1.61 % 1.40/1.61 ======= end of input processing ======= % 1.40/1.61 % 1.40/1.61 SEGMENTATION FAULT!! This is probably caused by a % 1.40/1.61 bug in Otter. Please send copy of the input file to % 1.40/1.61 otter@mcs.anl.gov, let us know what version of Otter you are % 1.40/1.61 using, and send any other info that might be useful. % 1.40/1.61 % 1.40/1.61 % 1.40/1.61 SEGMENTATION FAULT!! This is probably caused by a % 1.40/1.61 bug in Otter. Please send copy of the input file to % 1.40/1.61 otter@mcs.anl.gov, let us know what version of Otter you are % 1.40/1.61 using, and send any other info that might be useful. % 1.40/1.61 % 1.40/1.61 % 1.40/1.61 The job finished Sun Jul 3 06:46:38 2022 %------------------------------------------------------------------------------