%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SYN513+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %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 : 600s % DateTime : Thu Jul 21 03:03:10 EDT 2022 % Result : CounterSatisfiable 5.44s 5.62s % Output : FiniteModel 5.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : SYN513+1 : TPTP v8.1.0. Released v2.1.0. % 0.10/0.12 % Command : do_Crossbow---0.1 %s % 0.12/0.33 % Computer : n027.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.33 % DateTime : Tue Jul 12 03:16:34 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 /export/starexec/sandbox2/solver/bin % 0.12/0.33 crossbow.opt % 0.12/0.33 do_Crossbow---0.1 % 0.12/0.33 eprover % 0.12/0.33 runsolver % 0.12/0.33 starexec_run_Crossbow---0.1 % 5.44/5.62 % SZS status CounterSatisfiable for theBenchmark.p % 5.44/5.62 % SZS output start FiniteModel for theBenchmark.p % 5.44/5.62 % domain size: 3 % 5.44/5.62 fof(interp, fi_domain, ![X] : (X = 0 | X = 1 | X = 2)). % 5.44/5.62 fof(interp, fi_functors, a775 = 0). % 5.44/5.62 fof(interp, fi_functors, a776 = 0). % 5.44/5.62 fof(interp, fi_functors, a777 = 0). % 5.44/5.62 fof(interp, fi_functors, a778 = 0). % 5.44/5.62 fof(interp, fi_functors, a779 = 0). % 5.44/5.62 fof(interp, fi_functors, a780 = 0). % 5.44/5.62 fof(interp, fi_functors, a781 = 0). % 5.44/5.62 fof(interp, fi_functors, a782 = 0). % 5.44/5.62 fof(interp, fi_functors, a783 = 0). % 5.44/5.62 fof(interp, fi_functors, a784 = 1). % 5.44/5.62 fof(interp, fi_functors, a785 = 1). % 5.44/5.62 fof(interp, fi_functors, a786 = 1). % 5.44/5.62 fof(interp, fi_functors, a787 = 0). % 5.44/5.62 fof(interp, fi_functors, a788 = 2). % 5.44/5.62 fof(interp, fi_functors, a789 = 1). % 5.44/5.62 fof(interp, fi_functors, a790 = 2). % 5.44/5.62 fof(interp, fi_functors, a791 = 0). % 5.44/5.62 fof(interp, fi_functors, a792 = 0). % 5.44/5.62 fof(interp, fi_functors, a793 = 0). % 5.44/5.62 fof(interp, fi_functors, a794 = 0). % 5.44/5.62 fof(interp, fi_functors, a795 = 0). % 5.44/5.62 fof(interp, fi_functors, a796 = 0). % 5.44/5.62 fof(interp, fi_functors, a797 = 0). % 5.44/5.62 fof(interp, fi_functors, a798 = 0). % 5.44/5.62 fof(interp, fi_functors, a799 = 0). % 5.44/5.62 fof(interp, fi_functors, a800 = 2). % 5.44/5.62 fof(interp, fi_functors, a801 = 0). % 5.44/5.62 fof(interp, fi_functors, a802 = 0). % 5.44/5.62 fof(interp, fi_functors, a803 = 1). % 5.44/5.62 fof(interp, fi_functors, a804 = 0). % 5.44/5.62 fof(interp, fi_functors, a805 = 0). % 5.44/5.62 fof(interp, fi_functors, a806 = 1). % 5.44/5.62 fof(interp, fi_functors, a807 = 1). % 5.44/5.62 fof(interp, fi_functors, a808 = 0). % 5.44/5.62 fof(interp, fi_functors, a809 = 2). % 5.44/5.62 fof(interp, fi_functors, a810 = 0). % 5.44/5.62 fof(interp, fi_functors, a811 = 1). % 5.44/5.62 fof(interp, fi_functors, a812 = 2). % 5.44/5.62 fof(interp, fi_functors, a813 = 0). % 5.44/5.62 fof(interp, fi_functors, a814 = 0). % 5.44/5.62 fof(interp, fi_functors, a815 = 0). % 5.44/5.62 fof(interp, fi_functors, a816 = 0). % 5.44/5.62 fof(interp, fi_functors, a817 = 0). % 5.44/5.62 fof(interp, fi_functors, a818 = 1). % 5.44/5.62 fof(interp, fi_functors, a819 = 0). % 5.44/5.62 fof(interp, fi_functors, a820 = 0). % 5.44/5.62 fof(interp, fi_functors, a821 = 1). % 5.44/5.62 fof(interp, fi_functors, a822 = 0). % 5.44/5.62 fof(interp, fi_functors, a823 = 0). % 5.44/5.62 fof(interp, fi_functors, a824 = 1). % 5.44/5.62 fof(interp, fi_functors, a825 = 2). % 5.44/5.62 fof(interp, fi_functors, a826 = 2). % 5.44/5.62 fof(interp, fi_functors, a827 = 2). % 5.44/5.62 fof(interp, fi_functors, a828 = 2). % 5.44/5.62 fof(interp, fi_functors, a829 = 1). % 5.44/5.62 fof(interp, fi_functors, a830 = 2). % 5.44/5.62 fof(interp, fi_functors, a831 = 1). % 5.44/5.62 fof(interp, fi_functors, a832 = 1). % 5.44/5.62 fof(interp, fi_functors, a833 = 2). % 5.44/5.62 fof(interp, fi_functors, a834 = 0). % 5.44/5.62 fof(interp, fi_functors, a835 = 0). % 5.44/5.62 fof(interp, fi_functors, a836 = 0). % 5.44/5.62 fof(interp, fi_functors, a837 = 0). % 5.44/5.62 fof(interp, fi_functors, a838 = 0). % 5.44/5.62 fof(interp, fi_functors, a839 = 1). % 5.44/5.62 fof(interp, fi_functors, a840 = 1). % 5.44/5.62 fof(interp, fi_functors, a841 = 0). % 5.44/5.62 fof(interp, fi_functors, a842 = 0). % 5.44/5.62 fof(interp, fi_functors, a843 = 0). % 5.44/5.62 fof(interp, fi_functors, a844 = 0). % 5.44/5.62 fof(interp, fi_functors, a845 = 0). % 5.44/5.62 fof(interp, fi_functors, a846 = 0). % 5.44/5.62 fof(interp, fi_functors, a847 = 0). % 5.44/5.62 fof(interp, fi_functors, a848 = 0). % 5.44/5.62 fof(interp, fi_functors, a849 = 0). % 5.44/5.62 fof(interp, fi_functors, a850 = 0). % 5.44/5.62 fof(interp, fi_functors, a851 = 0). % 5.44/5.62 fof(interp, fi_functors, a852 = 0). % 5.44/5.62 fof(interp, fi_functors, a853 = 1). % 5.44/5.62 fof(interp, fi_functors, a854 = 1). % 5.44/5.62 fof(interp, fi_functors, a855 = 0). % 5.44/5.62 fof(interp, fi_functors, a856 = 0). % 5.44/5.62 fof(interp, fi_functors, a857 = 0). % 5.44/5.62 fof(interp, fi_functors, a858 = 1). % 5.44/5.62 fof(interp, fi_functors, a859 = 2). % 5.44/5.62 fof(interp, fi_functors, a860 = 0). % 5.44/5.62 fof(interp, fi_functors, a861 = 0). % 5.44/5.62 fof(interp, fi_functors, a862 = 0). % 5.44/5.62 fof(interp, fi_functors, a863 = 2). % 5.44/5.62 fof(interp, fi_functors, a864 = 0). % 5.44/5.62 fof(interp, fi_functors, a865 = 0). % 5.44/5.62 fof(interp, fi_functors, a866 = 0). % 5.44/5.62 fof(interp, fi_functors, a867 = 0). % 5.44/5.62 fof(interp, fi_functors, a868 = 0). % 5.44/5.62 fof(interp, fi_functors, a869 = 0). % 5.44/5.62 fof(interp, fi_functors, a870 = 0). % 5.44/5.62 fof(interp, fi_functors, a871 = 2). % 5.44/5.62 fof(interp, fi_functors, a872 = 0). % 5.44/5.62 fof(interp, fi_functors, a873 = 0). % 5.44/5.62 fof(interp, fi_functors, a874 = 0). % 5.44/5.62 fof(interp, fi_functors, a875 = 2). % 5.44/5.62 fof(interp, fi_functors, a876 = 0). % 5.44/5.62 fof(interp, fi_functors, a877 = 0). % 5.44/5.62 fof(interp, fi_functors, a878 = 0). % 5.44/5.62 fof(interp, fi_functors, a879 = 0). % 5.44/5.62 fof(interp, fi_functors, a880 = 0). % 5.44/5.62 fof(interp, fi_functors, a881 = 0). % 5.44/5.62 fof(interp, fi_functors, a882 = 0). % 5.44/5.62 fof(interp, fi_functors, a883 = 1). % 5.44/5.62 fof(interp, fi_functors, a884 = 0). % 5.44/5.62 fof(interp, fi_functors, a885 = 0). % 5.44/5.62 fof(interp, fi_functors, a886 = 2). % 5.44/5.62 fof(interp, fi_functors, a887 = 1). % 5.44/5.62 fof(interp, fi_functors, a888 = 1). % 5.44/5.62 fof(interp, fi_functors, a889 = 1). % 5.44/5.62 fof(interp, fi_functors, a890 = 1). % 5.44/5.62 fof(interp, fi_functors, a891 = 1). % 5.44/5.62 fof(interp, fi_functors, a892 = 0). % 5.44/5.62 fof(interp, fi_functors, a893 = 0). % 5.44/5.62 fof(interp, fi_functors, a894 = 1). % 5.44/5.62 fof(interp, fi_functors, a895 = 0). % 5.44/5.62 fof(interp, fi_functors, a896 = 0). % 5.44/5.62 fof(interp, fi_predicates, ~c1_0). % 5.44/5.62 fof(interp, fi_predicates, c1_1(0) & ~c1_1(1) & c1_1(2)). % 5.44/5.62 fof(interp, fi_predicates, c1_2(0, 0) & ~c1_2(0, 1) & c1_2(0, 2) & ~c1_2(1, 0) & % 5.44/5.62 ~c1_2(1, 1) & % 5.44/5.62 ~c1_2(1, 2) & % 5.44/5.62 c1_2(2, 0) & % 5.44/5.62 c1_2(2, 1) & % 5.44/5.62 ~c1_2(2, 2)). % 5.44/5.62 fof(interp, fi_predicates, ~c2_0). % 5.44/5.62 fof(interp, fi_predicates, ~c2_1(0) & ~c2_1(1) & c2_1(2)). % 5.44/5.62 fof(interp, fi_predicates, ~c2_2(0, 0) & c2_2(0, 1) & c2_2(0, 2) & ~c2_2(1, 0) & % 5.44/5.62 c2_2(1, 1) & % 5.44/5.62 c2_2(1, 2) & % 5.44/5.62 c2_2(2, 0) & % 5.44/5.62 c2_2(2, 1) & % 5.44/5.62 c2_2(2, 2)). % 5.44/5.62 fof(interp, fi_predicates, ~c3_0). % 5.44/5.62 fof(interp, fi_predicates, ~c3_1(0) & c3_1(1) & ~c3_1(2)). % 5.44/5.62 fof(interp, fi_predicates, c3_2(0, 0) & c3_2(0, 1) & ~c3_2(0, 2) & ~c3_2(1, 0) & % 5.44/5.62 c3_2(1, 1) & % 5.44/5.62 c3_2(1, 2) & % 5.44/5.62 c3_2(2, 0) & % 5.44/5.62 c3_2(2, 1) & % 5.44/5.62 ~c3_2(2, 2)). % 5.44/5.62 fof(interp, fi_predicates, ~c4_0). % 5.44/5.62 fof(interp, fi_predicates, c4_1(0) & ~c4_1(1) & ~c4_1(2)). % 5.44/5.62 fof(interp, fi_predicates, ~c4_2(0, 0) & c4_2(0, 1) & c4_2(0, 2) & ~c4_2(1, 0) & % 5.44/5.62 c4_2(1, 1) & % 5.44/5.62 c4_2(1, 2) & % 5.44/5.62 ~c4_2(2, 0) & % 5.44/5.62 ~c4_2(2, 1) & % 5.44/5.62 c4_2(2, 2)). % 5.44/5.62 fof(interp, fi_predicates, c5_0). % 5.44/5.62 fof(interp, fi_predicates, ~c5_1(0) & c5_1(1) & ~c5_1(2)). % 5.44/5.62 fof(interp, fi_predicates, ~c5_2(0, 0) & ~c5_2(0, 1) & c5_2(0, 2) & ~c5_2(1, 0) & % 5.44/5.62 ~c5_2(1, 1) & % 5.44/5.62 c5_2(1, 2) & % 5.44/5.62 ~c5_2(2, 0) & % 5.44/5.62 ~c5_2(2, 1) & % 5.44/5.62 c5_2(2, 2)). % 5.44/5.62 fof(interp, fi_predicates, epred1_0). % 5.44/5.62 fof(interp, fi_predicates, ~epred2_0). % 5.44/5.62 fof(interp, fi_predicates, ~epred3_0). % 5.44/5.62 fof(interp, fi_predicates, epred4_0). % 5.44/5.62 fof(interp, fi_predicates, epred5_0). % 5.44/5.62 fof(interp, fi_predicates, ndr1_0). % 5.44/5.62 fof(interp, fi_predicates, ndr1_1(0) & ndr1_1(1) & ndr1_1(2)). % 5.44/5.62 % SZS output end FiniteModel for theBenchmark.p % 5.44/5.62 % 20 lemma(s) from E % 5.44/5.62 % cnf(cl, axiom, c5_0). % 5.44/5.62 % cnf(cl, axiom, epred4_0). % 5.44/5.62 % cnf(cl, axiom, ~c4_0). % 5.44/5.62 % cnf(cl, axiom, ~c1_0). % 5.44/5.62 % cnf(cl, axiom, ~c2_0). % 5.44/5.62 % cnf(cl, axiom, c2_1(a830)). % 5.44/5.62 % cnf(cl, axiom, c5_1(a858)). % 5.44/5.62 % cnf(cl, axiom, c2_1(a800)). % 5.44/5.62 % cnf(cl, axiom, ndr1_1(A)). % 5.44/5.62 % cnf(cl, axiom, c3_2(a853, a854)). % 5.44/5.62 % cnf(cl, axiom, c2_2(a839, a840)). % 5.44/5.62 % cnf(cl, axiom, c2_2(a853, a854)). % 5.44/5.62 % cnf(cl, axiom, c3_2(a858, a859)). % 5.44/5.62 % cnf(cl, axiom, c4_2(a839, a840)). % 5.44/5.62 % cnf(cl, axiom, c2_2(a858, a859)). % 5.44/5.62 % cnf(cl, axiom, ~c4_2(a839, a841)). % 5.44/5.62 % cnf(cl, axiom, ~c5_2(a839, a840)). % 5.44/5.62 % cnf(cl, axiom, ~c2_2(a839, a841)). % 5.44/5.62 % cnf(cl, axiom, ~c1_2(a858, a859)). % 5.44/5.62 % cnf(cl, axiom, ~c5_2(a839, a841)). % 5.44/5.62 % 674 pred(s) % 5.44/5.62 % 122 func(s) % 5.44/5.62 % 2 sort(s) % 5.44/5.62 % 1657 clause(s) % 5.44/5.62 % Instantiating 1 (5202 ms) % 5.44/5.62 % Solving (5203 ms) % 5.44/5.62 % Instantiating 2 (5203 ms) % 5.44/5.62 % Solving (5207 ms) % 5.44/5.62 % Instantiating 3 (5208 ms) % 5.44/5.62 % Solving (5216 ms) % 5.44/5.62 % % 5.44/5.62 % 1 model found (5218 ms) %------------------------------------------------------------------------------