%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SYO579+1 : TPTP v8.1.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n021.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 14:34:26 EDT 2022 % Result : CounterSatisfiable 1.27s 1.51s % Output : FiniteModel 1.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYO579+1 : TPTP v8.1.0. Released v5.5.0. % 0.06/0.12 % Command : do_Crossbow---0.1 %s % 0.12/0.34 % Computer : n021.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 % WCLimit : 600 % 0.12/0.34 % DateTime : Sat Jul 9 13:50:36 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 /export/starexec/sandbox/solver/bin % 0.12/0.34 crossbow.opt % 0.12/0.34 do_Crossbow---0.1 % 0.12/0.34 eprover % 0.12/0.34 runsolver % 0.12/0.34 starexec_run_Crossbow---0.1 % 1.27/1.51 % SZS status CounterSatisfiable for theBenchmark.p % 1.27/1.51 % SZS output start FiniteModel for theBenchmark.p % 1.27/1.51 % domain size: 7 % 1.27/1.51 fof(interp, fi_domain, ![X] : (X = 0 | X = 1 | X = 2 | X = 3 | X = 4 | X = 5 | % 1.27/1.51 X = 6)). % 1.27/1.51 fof(interp, fi_predicates, b48_buttercup10098(0) & b48_buttercup10098(1) & % 1.27/1.51 b48_buttercup10098(2) & % 1.27/1.51 b48_buttercup10098(3) & % 1.27/1.51 b48_buttercup10098(4) & % 1.27/1.51 b48_buttercup10098(5) & % 1.27/1.51 b48_buttercup10098(6)). % 1.27/1.51 fof(interp, fi_predicates, ~b48_buttercup10102(0) & b48_buttercup10102(1) & % 1.27/1.51 ~b48_buttercup10102(2) & % 1.27/1.51 ~b48_buttercup10102(3) & % 1.27/1.51 ~b48_buttercup10102(4) & % 1.27/1.51 ~b48_buttercup10102(5) & % 1.27/1.51 ~b48_buttercup10102(6)). % 1.27/1.51 fof(interp, fi_predicates, ~b48_buttercup10104(0) & ~b48_buttercup10104(1) & % 1.27/1.51 ~b48_buttercup10104(2) & % 1.27/1.51 ~b48_buttercup10104(3) & % 1.27/1.51 ~b48_buttercup10104(4) & % 1.27/1.51 ~b48_buttercup10104(5) & % 1.27/1.51 b48_buttercup10104(6)). % 1.27/1.51 fof(interp, fi_predicates, b48_buttercup10107(0) & ~b48_buttercup10107(1) & % 1.27/1.51 ~b48_buttercup10107(2) & % 1.27/1.51 ~b48_buttercup10107(3) & % 1.27/1.51 ~b48_buttercup10107(4) & % 1.27/1.51 ~b48_buttercup10107(5) & % 1.27/1.51 ~b48_buttercup10107(6)). % 1.27/1.51 fof(interp, fi_predicates, ~b48_buttercup10108(0) & ~b48_buttercup10108(1) & % 1.27/1.51 ~b48_buttercup10108(2) & % 1.27/1.51 ~b48_buttercup10108(3) & % 1.27/1.51 b48_buttercup10108(4) & % 1.27/1.51 ~b48_buttercup10108(5) & % 1.27/1.51 ~b48_buttercup10108(6)). % 1.27/1.51 fof(interp, fi_predicates, ~b48_buttercup10109(0) & ~b48_buttercup10109(1) & % 1.27/1.51 ~b48_buttercup10109(2) & % 1.27/1.51 b48_buttercup10109(3) & % 1.27/1.51 ~b48_buttercup10109(4) & % 1.27/1.51 ~b48_buttercup10109(5) & % 1.27/1.51 ~b48_buttercup10109(6)). % 1.27/1.51 fof(interp, fi_predicates, ~b48_buttercup10110(0) & ~b48_buttercup10110(1) & % 1.27/1.51 b48_buttercup10110(2) & % 1.27/1.51 ~b48_buttercup10110(3) & % 1.27/1.51 ~b48_buttercup10110(4) & % 1.27/1.51 ~b48_buttercup10110(5) & % 1.27/1.51 ~b48_buttercup10110(6)). % 1.27/1.51 fof(interp, fi_predicates, ~b48_buttercup10111(0) & ~b48_buttercup10111(1) & % 1.27/1.51 ~b48_buttercup10111(2) & % 1.27/1.51 ~b48_buttercup10111(3) & % 1.27/1.51 ~b48_buttercup10111(4) & % 1.27/1.51 b48_buttercup10111(5) & % 1.27/1.51 ~b48_buttercup10111(6)). % 1.27/1.51 fof(interp, fi_predicates, ~epred1_0). % 1.27/1.51 fof(interp, fi_predicates, ~epred2_0). % 1.27/1.51 fof(interp, fi_predicates, ~epred3_0). % 1.27/1.51 fof(interp, fi_predicates, ~epred4_0). % 1.27/1.51 fof(interp, fi_predicates, ~epred5_0). % 1.27/1.51 fof(interp, fi_predicates, ~epred6_0). % 1.27/1.51 fof(interp, fi_predicates, ~epred7_0). % 1.27/1.51 fof(interp, fi_functors, esk10_0 = 1). % 1.27/1.51 fof(interp, fi_functors, esk11_0 = 0). % 1.27/1.51 fof(interp, fi_functors, esk12_0 = 1). % 1.27/1.51 fof(interp, fi_functors, esk13_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk14_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk15_0 = 2). % 1.27/1.51 fof(interp, fi_functors, esk16_0 = 1). % 1.27/1.51 fof(interp, fi_functors, esk17_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk18_0 = 0). % 1.27/1.51 fof(interp, fi_functors, esk19_0 = 4). % 1.27/1.51 fof(interp, fi_functors, esk1_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk20_0 = 3). % 1.27/1.51 fof(interp, fi_functors, esk21_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk22_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk23_0 = 0). % 1.27/1.51 fof(interp, fi_functors, esk24_0 = 0). % 1.27/1.51 fof(interp, fi_functors, esk25_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk26_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk27_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk28_0 = 1). % 1.27/1.51 fof(interp, fi_functors, esk29_0 = 1). % 1.27/1.51 fof(interp, fi_functors, esk2_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk30_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk31_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk32_0 = 1). % 1.27/1.51 fof(interp, fi_functors, esk33_0 = 1). % 1.27/1.51 fof(interp, fi_functors, esk34_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk35_0 = 0). % 1.27/1.51 fof(interp, fi_functors, esk36_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk37_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk38_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk39_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk3_0 = 3). % 1.27/1.51 fof(interp, fi_functors, esk40_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk41_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk42_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk43_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk44_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk45_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk46_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk47_0 = 0). % 1.27/1.51 fof(interp, fi_functors, esk48_0 = 0). % 1.27/1.51 fof(interp, fi_functors, esk49_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk4_0 = 1). % 1.27/1.51 fof(interp, fi_functors, esk50_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk51_0 = 0). % 1.27/1.51 fof(interp, fi_functors, esk52_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk53_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk54_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk55_0 = 5). % 1.27/1.51 fof(interp, fi_functors, esk56_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk5_0 = 1). % 1.27/1.51 fof(interp, fi_functors, esk6_0 = 2). % 1.27/1.51 fof(interp, fi_functors, esk7_0 = 6). % 1.27/1.51 fof(interp, fi_functors, esk8_0 = 2). % 1.27/1.51 fof(interp, fi_functors, esk9_0 = 5). % 1.27/1.51 fof(interp, fi_predicates, ~k04_buttercup10100(0) & ~k04_buttercup10100(1) & % 1.27/1.51 ~k04_buttercup10100(2) & % 1.27/1.51 k04_buttercup10100(3) & % 1.27/1.51 ~k04_buttercup10100(4) & % 1.27/1.51 k04_buttercup10100(5) & % 1.27/1.51 ~k04_buttercup10100(6)). % 1.27/1.51 fof(interp, fi_predicates, k04_buttercup10619(0) & k04_buttercup10619(1) & % 1.27/1.51 k04_buttercup10619(2) & % 1.27/1.51 ~k04_buttercup10619(3) & % 1.27/1.51 k04_buttercup10619(4) & % 1.27/1.51 ~k04_buttercup10619(5) & % 1.27/1.51 k04_buttercup10619(6)). % 1.27/1.51 fof(interp, fi_predicates, k04_buttercup10620(0) & ~k04_buttercup10620(1) & % 1.27/1.51 ~k04_buttercup10620(2) & % 1.27/1.51 ~k04_buttercup10620(3) & % 1.27/1.51 ~k04_buttercup10620(4) & % 1.27/1.51 ~k04_buttercup10620(5) & % 1.27/1.51 ~k04_buttercup10620(6)). % 1.27/1.51 fof(interp, fi_predicates, ~k04_buttercup10622(0) & k04_buttercup10622(1) & % 1.27/1.51 k04_buttercup10622(2) & % 1.27/1.51 ~k04_buttercup10622(3) & % 1.27/1.51 k04_buttercup10622(4) & % 1.27/1.51 ~k04_buttercup10622(5) & % 1.27/1.51 k04_buttercup10622(6)). % 1.27/1.51 % SZS output end FiniteModel for theBenchmark.p % 1.27/1.51 % 20 lemma(s) from E % 1.27/1.51 % cnf(cl, axiom, ~epred3_0). % 1.27/1.51 % cnf(cl, axiom, ~epred2_0). % 1.27/1.51 % cnf(cl, axiom, ~epred6_0). % 1.27/1.51 % cnf(cl, axiom, ~epred1_0). % 1.27/1.51 % cnf(cl, axiom, ~epred7_0). % 1.27/1.51 % cnf(cl, axiom, ~epred4_0). % 1.27/1.51 % cnf(cl, axiom, ~epred5_0). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10620(esk18_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10619(esk12_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10619(esk8_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10619(esk6_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10619(esk5_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10619(esk4_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10622(esk16_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10619(esk16_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10622(esk17_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10619(esk17_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10622(esk19_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10619(esk19_0)). % 1.27/1.51 % cnf(cl, axiom, k04_buttercup10622(esk15_0)). % 1.27/1.51 % 19 pred(s) % 1.27/1.51 % 56 func(s) % 1.27/1.51 % 1 sort(s) % 1.27/1.51 % 502 clause(s) % 1.27/1.51 % Instantiating 1 (1021 ms) % 1.27/1.51 % Solving (1022 ms) % 1.27/1.51 % Instantiating 2 (1022 ms) % 1.27/1.51 % Solving (1025 ms) % 1.27/1.51 % Instantiating 3 (1025 ms) % 1.27/1.51 % Solving (1032 ms) % 1.27/1.51 % Instantiating 4 (1032 ms) % 1.27/1.51 % Solving (1046 ms) % 1.27/1.51 % Instantiating 5 (1046 ms) % 1.27/1.51 % Solving (1068 ms) % 1.27/1.51 % Instantiating 6 (1068 ms) % 1.27/1.51 % Solving (1098 ms) % 1.27/1.51 % Instantiating 7 (1099 ms) % 1.27/1.51 % Solving (1126 ms) % 1.27/1.51 % % 1.27/1.51 % 1 model found (1126 ms) %------------------------------------------------------------------------------