%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SYN542+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n008.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:31 EDT 2022 % Result : CounterSatisfiable 5.25s 5.43s % Output : FiniteModel 5.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN542+1 : TPTP v8.1.0. Released v2.1.0. % 0.07/0.13 % Command : do_Crossbow---0.1 %s % 0.13/0.34 % Computer : n008.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jul 11 22:51:53 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.35 /export/starexec/sandbox/solver/bin % 0.13/0.35 crossbow.opt % 0.13/0.35 do_Crossbow---0.1 % 0.13/0.35 eprover % 0.13/0.35 runsolver % 0.13/0.35 starexec_run_Crossbow---0.1 % 5.25/5.43 % SZS status CounterSatisfiable for theBenchmark.p % 5.25/5.43 % SZS output start FiniteModel for theBenchmark.p % 5.25/5.43 % domain size: 3 % 5.25/5.43 fof(interp, fi_domain, ![X] : (X = 0 | X = 1 | X = 2)). % 5.25/5.43 fof(interp, fi_functors, a1 = 0). % 5.25/5.43 fof(interp, fi_functors, a10 = 2). % 5.25/5.43 fof(interp, fi_functors, a11 = 2). % 5.25/5.43 fof(interp, fi_functors, a12 = 1). % 5.25/5.43 fof(interp, fi_functors, a14 = 2). % 5.25/5.43 fof(interp, fi_functors, a15 = 0). % 5.25/5.43 fof(interp, fi_functors, a17 = 0). % 5.25/5.43 fof(interp, fi_functors, a19 = 2). % 5.25/5.43 fof(interp, fi_functors, a2 = 0). % 5.25/5.43 fof(interp, fi_functors, a20 = 0). % 5.25/5.43 fof(interp, fi_functors, a21 = 0). % 5.25/5.43 fof(interp, fi_functors, a22 = 0). % 5.25/5.43 fof(interp, fi_functors, a23 = 0). % 5.25/5.43 fof(interp, fi_functors, a24 = 2). % 5.25/5.43 fof(interp, fi_functors, a25 = 0). % 5.25/5.43 fof(interp, fi_functors, a26 = 2). % 5.25/5.43 fof(interp, fi_functors, a27 = 2). % 5.25/5.43 fof(interp, fi_functors, a28 = 2). % 5.25/5.43 fof(interp, fi_functors, a29 = 2). % 5.25/5.43 fof(interp, fi_functors, a3 = 1). % 5.25/5.43 fof(interp, fi_functors, a30 = 2). % 5.25/5.43 fof(interp, fi_functors, a31 = 1). % 5.25/5.43 fof(interp, fi_functors, a32 = 2). % 5.25/5.43 fof(interp, fi_functors, a33 = 2). % 5.25/5.43 fof(interp, fi_functors, a34 = 2). % 5.25/5.43 fof(interp, fi_functors, a35 = 0). % 5.25/5.43 fof(interp, fi_functors, a36 = 0). % 5.25/5.43 fof(interp, fi_functors, a37 = 0). % 5.25/5.43 fof(interp, fi_functors, a4 = 0). % 5.25/5.43 fof(interp, fi_functors, a40 = 0). % 5.25/5.43 fof(interp, fi_functors, a41 = 0). % 5.25/5.43 fof(interp, fi_functors, a42 = 0). % 5.25/5.43 fof(interp, fi_functors, a44 = 2). % 5.25/5.43 fof(interp, fi_functors, a45 = 2). % 5.25/5.43 fof(interp, fi_functors, a46 = 2). % 5.25/5.43 fof(interp, fi_functors, a47 = 2). % 5.25/5.43 fof(interp, fi_functors, a49 = 0). % 5.25/5.43 fof(interp, fi_functors, a5 = 1). % 5.25/5.43 fof(interp, fi_functors, a50 = 2). % 5.25/5.43 fof(interp, fi_functors, a51 = 2). % 5.25/5.43 fof(interp, fi_functors, a54 = 2). % 5.25/5.43 fof(interp, fi_functors, a56 = 1). % 5.25/5.43 fof(interp, fi_functors, a59 = 1). % 5.25/5.43 fof(interp, fi_functors, a6 = 0). % 5.25/5.43 fof(interp, fi_functors, a60 = 1). % 5.25/5.43 fof(interp, fi_functors, a61 = 2). % 5.25/5.43 fof(interp, fi_functors, a62 = 2). % 5.25/5.43 fof(interp, fi_functors, a63 = 0). % 5.25/5.43 fof(interp, fi_functors, a64 = 2). % 5.25/5.43 fof(interp, fi_functors, a66 = 0). % 5.25/5.43 fof(interp, fi_functors, a67 = 2). % 5.25/5.43 fof(interp, fi_functors, a68 = 2). % 5.25/5.43 fof(interp, fi_functors, a7 = 0). % 5.25/5.43 fof(interp, fi_functors, a71 = 2). % 5.25/5.43 fof(interp, fi_functors, a73 = 2). % 5.25/5.43 fof(interp, fi_functors, a75 = 0). % 5.25/5.43 fof(interp, fi_functors, a76 = 0). % 5.25/5.43 fof(interp, fi_functors, a8 = 2). % 5.25/5.43 fof(interp, fi_functors, a9 = 1). % 5.25/5.43 fof(interp, fi_predicates, c0_1(0) & ~c0_1(1) & ~c0_1(2)). % 5.25/5.43 fof(interp, fi_predicates, ~c1_1(0) & c1_1(1) & c1_1(2)). % 5.25/5.43 fof(interp, fi_predicates, c2_1(0) & ~c2_1(1) & ~c2_1(2)). % 5.25/5.43 fof(interp, fi_predicates, c3_1(0) & ~c3_1(1) & c3_1(2)). % 5.25/5.43 fof(interp, fi_predicates, c4_1(0) & c4_1(1) & ~c4_1(2)). % 5.25/5.43 fof(interp, fi_predicates, c5_1(0) & ~c5_1(1) & c5_1(2)). % 5.25/5.43 fof(interp, fi_predicates, ~hskp0). % 5.25/5.43 fof(interp, fi_predicates, hskp1). % 5.25/5.43 fof(interp, fi_predicates, ~hskp10). % 5.25/5.43 fof(interp, fi_predicates, hskp11). % 5.25/5.43 fof(interp, fi_predicates, ~hskp12). % 5.25/5.43 fof(interp, fi_predicates, ~hskp13). % 5.25/5.43 fof(interp, fi_predicates, ~hskp14). % 5.25/5.43 fof(interp, fi_predicates, ~hskp15). % 5.25/5.43 fof(interp, fi_predicates, ~hskp16). % 5.25/5.43 fof(interp, fi_predicates, hskp17). % 5.25/5.43 fof(interp, fi_predicates, ~hskp18). % 5.25/5.43 fof(interp, fi_predicates, ~hskp19). % 5.25/5.43 fof(interp, fi_predicates, hskp2). % 5.25/5.43 fof(interp, fi_predicates, ~hskp20). % 5.25/5.43 fof(interp, fi_predicates, ~hskp21). % 5.25/5.43 fof(interp, fi_predicates, ~hskp22). % 5.25/5.43 fof(interp, fi_predicates, ~hskp23). % 5.25/5.43 fof(interp, fi_predicates, hskp24). % 5.25/5.43 fof(interp, fi_predicates, ~hskp25). % 5.25/5.43 fof(interp, fi_predicates, hskp26). % 5.25/5.43 fof(interp, fi_predicates, ~hskp27). % 5.25/5.43 fof(interp, fi_predicates, hskp28). % 5.25/5.43 fof(interp, fi_predicates, ~hskp29). % 5.25/5.43 fof(interp, fi_predicates, ~hskp3). % 5.25/5.43 fof(interp, fi_predicates, ~hskp30). % 5.25/5.43 fof(interp, fi_predicates, ~hskp31). % 5.25/5.43 fof(interp, fi_predicates, ~hskp32). % 5.25/5.43 fof(interp, fi_predicates, ~hskp33). % 5.25/5.43 fof(interp, fi_predicates, ~hskp34). % 5.25/5.43 fof(interp, fi_predicates, ~hskp35). % 5.25/5.43 fof(interp, fi_predicates, ~hskp36). % 5.25/5.43 fof(interp, fi_predicates, ~hskp37). % 5.25/5.43 fof(interp, fi_predicates, ~hskp38). % 5.25/5.43 fof(interp, fi_predicates, hskp39). % 5.25/5.43 fof(interp, fi_predicates, ~hskp4). % 5.25/5.43 fof(interp, fi_predicates, ~hskp40). % 5.25/5.43 fof(interp, fi_predicates, hskp41). % 5.25/5.43 fof(interp, fi_predicates, hskp42). % 5.25/5.43 fof(interp, fi_predicates, ~hskp43). % 5.25/5.43 fof(interp, fi_predicates, ~hskp44). % 5.25/5.43 fof(interp, fi_predicates, hskp45). % 5.25/5.43 fof(interp, fi_predicates, ~hskp46). % 5.25/5.43 fof(interp, fi_predicates, hskp47). % 5.25/5.43 fof(interp, fi_predicates, ~hskp48). % 5.25/5.43 fof(interp, fi_predicates, ~hskp49). % 5.25/5.43 fof(interp, fi_predicates, ~hskp5). % 5.25/5.43 fof(interp, fi_predicates, hskp50). % 5.25/5.43 fof(interp, fi_predicates, ~hskp51). % 5.25/5.43 fof(interp, fi_predicates, ~hskp52). % 5.25/5.43 fof(interp, fi_predicates, ~hskp53). % 5.25/5.43 fof(interp, fi_predicates, ~hskp54). % 5.25/5.43 fof(interp, fi_predicates, ~hskp55). % 5.25/5.43 fof(interp, fi_predicates, ~hskp56). % 5.25/5.43 fof(interp, fi_predicates, hskp57). % 5.25/5.43 fof(interp, fi_predicates, ~hskp58). % 5.25/5.43 fof(interp, fi_predicates, hskp6). % 5.25/5.43 fof(interp, fi_predicates, ~hskp7). % 5.25/5.43 fof(interp, fi_predicates, ~hskp8). % 5.25/5.43 fof(interp, fi_predicates, ~hskp9). % 5.25/5.43 fof(interp, fi_predicates, ndr1_0). % 5.25/5.43 % SZS output end FiniteModel for theBenchmark.p % 5.25/5.43 % 0 lemma(s) from E % 5.25/5.43 % 66 pred(s) % 5.25/5.43 % 59 func(s) % 5.25/5.43 % 1 sort(s) % 5.25/5.43 % 290 clause(s) % 5.25/5.43 % Instantiating 1 (5037 ms) % 5.25/5.43 % Solving (5038 ms) % 5.25/5.43 % Instantiating 2 (5038 ms) % 5.25/5.43 % Solving (5039 ms) % 5.25/5.43 % Instantiating 3 (5040 ms) % 5.25/5.43 % Solving (5041 ms) % 5.25/5.43 % % 5.25/5.43 % 1 model found (5042 ms) %------------------------------------------------------------------------------