%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : AGT042+1 : TPTP v9.2.1. Released v6.4.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n029.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 : 300s % DateTime : Thu May 7 07:17:20 PM UTC 2026 % Result : Satisfiable 4.24s 1.38s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : AGT042+1 : TPTP v9.2.1. Released v6.4.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n029.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Thu May 7 14:03:15 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 4.24/1.37 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.24/1.37 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.24/1.37 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.24/1.37 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.24/1.37 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.24/1.37 Execution lmodel_grow ended with status: satisfiable % 4.24/1.37 Used heuristic: lmodel_grow % 4.24/1.37 % 4.24/1.37 Input Clauses: % 4.24/1.37 % 4.24/1.37 Predicates: accept_team accept_city accept_leader accept_number less accept_population the_agent_in_all_proposed_teams any_agent_in_all_proposed_teams the_agent_not_in_any_proposed_teams min_number_of_proposed_agents ren1 % 4.24/1.37 Fol Constants: atheist n65 christian n20 muslim n7 native n4 other suffertown n54 n23 n3 n1 n9 centraltown n30 n8 n60 sunnysideport n70 n15 n10 centrallakecity n68 n16 n11 stjosephburgh n13 n0 n2 northport n12 n85 coastvillage n100 sunsetpoint n75 n24 towna n25 citya townb n78 cityb n5 townc countryahumanitarianorganization countryacivilorganization n6 countryafirstaidorganization christiancountrychumanitarianorganization countryccivilorganization countrybhumanitarianorganization muslimcountrybhumanitarianorganization countrycmedicalorganization countryamedicalorganization countrybcivilorganization christiansufferterrahumanitarianorganization sufferterragovernment % 4.24/1.37 Fol Functions: % 4.24/1.37 Problem Properties: % 4.24/1.37 This is a Bernays Schoenfinkel problem. % 4.24/1.37 % 4.24/1.37 After reduction: Problem Properties: % 4.24/1.37 This is a Bernays Schoenfinkel problem. % 4.24/1.37 % 4.24/1.37 % 4.24/1.37 Reduced Input Clauses: % 4.24/1.38 % 4.24/1.38 Most General Atoms: accept_city(x0,x1) accept_leader(x0,x2) accept_team(x0,x2,x1,x3) accept_number(x0,x2) less(x3,x2) accept_population(x0,x1,x3) ren1(x0,x1,x2) the_agent_in_all_proposed_teams(x0,x1,x2) any_agent_in_all_proposed_teams(x0,x1,x2) the_agent_not_in_any_proposed_teams(x0,x1,x2) min_number_of_proposed_agents(x0,x1) % 4.24/1.38 % 4.24/1.38 === Starting SPASS-SCL-FOL A Little Less Naive, considering 643 atoms initially, heuristics mode: lmodel_grow === % 4.24/1.38 % 4.24/1.38 === Backtracking. Learning clause 707:2:3:[11.3,7.2,8.2,9.2]:TopTopTop: the_agent_not_in_any_proposed_teams(x0,x1,x2),the_agent_in_all_proposed_teams(x0,x1,x2) -> % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 665 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 677 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 682 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 687 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 690 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 694 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 697 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 699 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 702 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 704 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 707 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 716 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 720 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 722 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 724 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 727 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 729 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 732 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 735 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 738 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 741 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 744 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 747 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 750 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 753 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 755 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 758 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 760 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 766 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 769 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 770 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 772 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 774 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 776 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 778 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 780 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 781 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 783 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 784 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 785 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 786 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 787 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 788 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 789 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 790 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 802 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 806 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 807 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 808 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 809 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 810 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 811 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 813 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 816 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 817 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 818 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 820 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 823 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 824 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 825 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 826 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 827 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 829 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 832 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 833 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 834 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 835 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 836 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 837 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 838 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 839 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 840 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 841 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 842 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 843 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 844 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 845 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 846 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 847 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 848 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 849 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 850 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 855 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 856 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 857 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 858 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 859 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 860 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 861 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 862 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 863 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 864 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 865 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 866 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 867 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 868 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 869 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 870 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 871 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 873 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 876 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 879 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 882 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 885 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 888 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 891 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 895 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 896 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 897 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 898 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 899 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 900 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 903 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 906 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 910 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 914 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 918 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 920 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 921 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 922 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 923 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 924 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 925 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 926 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 927 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 928 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 929 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 930 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 931 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 932 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 933 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 934 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 935 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 936 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 937 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 938 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 939 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 940 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 941 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 944 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 948 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 950 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 952 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 953 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 954 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 955 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 956 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 957 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 958 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 959 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 960 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 961 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 964 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 966 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 967 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 968 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 969 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 970 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 971 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 972 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 973 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 974 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 975 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 977 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 979 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 980 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 981 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 982 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 983 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 984 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 985 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 986 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 987 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 988 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 989 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 990 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 991 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 992 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 993 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 994 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 996 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 998 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 999 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1000 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1001 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1002 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1003 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1004 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1005 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1006 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1007 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1008 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1017 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1019 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1020 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1021 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1022 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1023 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1024 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1025 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1026 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1027 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1028 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1029 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1031 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1032 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1033 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1034 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1035 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1036 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1037 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1038 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1039 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1040 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1041 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1042 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1043 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1044 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1045 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1046 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1047 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1049 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1051 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1052 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1053 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1054 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1055 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1056 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1057 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1058 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1059 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1060 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1061 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1063 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1065 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1066 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1067 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1068 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1069 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1070 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1071 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1072 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1073 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1074 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1075 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1077 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1078 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1079 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1080 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1081 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1082 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1083 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1084 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1085 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1086 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1087 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1088 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1090 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1091 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1092 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1093 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1094 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1095 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1096 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1097 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1098 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1099 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1100 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1101 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1102 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1103 % 4.24/1.38 === Clause set with instances from active satisfied. Growing active. New size: 1104 % 4.24/1.38 % 4.24/1.38 Linear Model Building succeeded. % 4.24/1.38 SZS status Satisfiable % 4.24/1.38 % 4.24/1.38 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 4.24/1.38 % 4.24/1.38 SPASS-SCL-FOL Statistics: % 4.24/1.38 Number of learned clauses: 1 % 4.24/1.38 Number of propagations: 1563 % 4.24/1.38 Number of decisions: 139 % 4.24/1.38 Number of resolutions: 3 % 4.24/1.38 Number of condensations: 0 % 4.24/1.38 Number of sub resolutions: 0 % 4.24/1.38 Number of input literals (deduplicated): 643 % 4.24/1.38 Number of grows: 272 % 4.24/1.38 Number of considered ground atoms: 1104 % 4.24/1.38 % 4.24/1.38 Needed: 0:00:00.84 % 4.24/1.38 %------------------------------------------------------------------------------