%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : SEV440^1 : TPTP v9.2.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n012.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 : Wed Jun 3 08:56:46 AM UTC 2026 % Result : Satisfiable 0.15s 0.35s % Output : Model 0.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SEV440^1 : TPTP v9.2.1. Released v6.4.0. % 0.00/0.07 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.25 % Computer : n012.cluster.edu % 0.06/0.25 % Model : x86_64 x86_64 % 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.25 % Memory : 8042.1875MB % 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.25 % CPULimit : 300 % 0.06/0.25 % WCLimit : 300 % 0.06/0.25 % DateTime : Tue Jun 2 18:32:48 EDT 2026 % 0.06/0.25 % CPUTime : % 0.15/0.33 %----Disproving TH0 % 0.15/0.34 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 72s... % 0.15/0.35 % SZS status Satisfiable % 0.15/0.35 % SZS output start Model % 0.15/0.35 ( % 0.15/0.35 ; cardinality of $$unsorted is 1 % 0.15/0.35 ; rep: (as @$$unsorted_0 $$unsorted) % 0.15/0.35 (define-fun tptp.in ((X $$unsorted) (M (-> $$unsorted Bool))) Bool (@ M X)) % 0.15/0.35 (define-fun tptp.is_a ((X $$unsorted) (M (-> $$unsorted Bool))) Bool (@ M X)) % 0.15/0.35 (define-fun tptp.emptyset ((BOUND_VARIABLE_1183 $$unsorted)) Bool false) % 0.15/0.35 (define-fun tptp.unord_pair ((X $$unsorted) (Y $$unsorted) (U $$unsorted)) Bool (or (= X U) (= Y U))) % 0.15/0.35 (define-fun tptp.singleton ((X $$unsorted) (U $$unsorted)) Bool (= X U)) % 0.15/0.35 (define-fun tptp.union ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool)) (U $$unsorted)) Bool (or (@ X U) (@ Y U))) % 0.15/0.35 (define-fun tptp.excl_union ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool)) (U $$unsorted)) Bool (or (and (@ X U) (not (@ Y U))) (and (not (@ X U)) (@ Y U)))) % 0.15/0.35 (define-fun tptp.intersection ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool)) (U $$unsorted)) Bool (and (@ X U) (@ Y U))) % 0.15/0.35 (define-fun tptp.setminus ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool)) (U $$unsorted)) Bool (and (@ X U) (not (@ Y U)))) % 0.15/0.35 (define-fun tptp.complement ((X (-> $$unsorted Bool)) (U $$unsorted)) Bool (not (@ X U))) % 0.15/0.35 (define-fun tptp.disjoint ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool))) Bool (= (lambda ((U $$unsorted)) (and (@ X U) (@ Y U))) (lambda ((BOUND_VARIABLE_1183 $$unsorted)) false))) % 0.15/0.35 (define-fun tptp.subset ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool))) Bool (forall ((U $$unsorted)) (or (not (X U)) (Y U)))) % 0.15/0.35 (define-fun tptp.meets ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool))) Bool (not (forall ((U $$unsorted)) (or (not (X U)) (not (Y U)))))) % 0.15/0.35 (define-fun tptp.misses ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool))) Bool (forall ((U $$unsorted)) (or (not (X U)) (not (Y U))))) % 0.15/0.35 (define-fun tptp.fun_image ((F (-> $$unsorted $$unsorted)) (A (-> $$unsorted Bool)) (Y $$unsorted)) Bool (not (forall ((X $$unsorted)) (or (not (A X)) (not (= Y (F X))))))) % 0.15/0.35 (define-fun tptp.fun_composition ((F (-> $$unsorted $$unsorted)) (G (-> $$unsorted $$unsorted)) (X $$unsorted)) $$unsorted (@ G (@ F X))) % 0.15/0.35 (define-fun tptp.fun_inv_image ((F (-> $$unsorted $$unsorted)) (B (-> $$unsorted Bool)) (X $$unsorted)) Bool (B (F X))) % 0.15/0.35 (define-fun tptp.fun_injective ((F (-> $$unsorted $$unsorted))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (= (F X) (F Y))) (= X Y)))) % 0.15/0.35 (define-fun tptp.fun_surjective ((F (-> $$unsorted $$unsorted))) Bool (forall ((Y $$unsorted)) (not (forall ((X $$unsorted)) (not (= Y (F X))))))) % 0.15/0.35 (define-fun tptp.fun_bijective ((F (-> $$unsorted $$unsorted))) Bool (and (forall ((X $$unsorted) (Y $$unsorted)) (or (not (= (F X) (F Y))) (= X Y))) (forall ((Y $$unsorted)) (not (forall ((X $$unsorted)) (not (= Y (F X)))))))) % 0.15/0.35 (define-fun tptp.fun_decreasing ((F (-> $$unsorted $$unsorted)) (SMALLER (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (SMALLER X Y)) (SMALLER (F Y) (F X))))) % 0.15/0.35 (define-fun tptp.fun_increasing ((F (-> $$unsorted $$unsorted)) (SMALLER (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (SMALLER X Y)) (SMALLER (F X) (F Y))))) % 0.15/0.35 (define-fun tptp.cartesian_product ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool)) (U $$unsorted) (V $$unsorted)) Bool (and (@ X U) (@ Y V))) % 0.15/0.35 (define-fun tptp.pair_rel ((X $$unsorted) (Y $$unsorted) (U $$unsorted) (V $$unsorted)) Bool (or (= X U) (= Y V))) % 0.15/0.35 (define-fun tptp.id_rel ((S (-> $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (and (@ S X) (= X Y))) % 0.15/0.35 (define-fun tptp.sub_rel ((R1 (-> $$unsorted $$unsorted Bool)) (R2 (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R1 X Y)) (R2 X Y)))) % 0.15/0.35 (define-fun tptp.is_rel_on ((R (-> $$unsorted $$unsorted Bool)) (A (-> $$unsorted Bool)) (B (-> $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (and (A X) (B Y))))) % 0.15/0.35 (define-fun tptp.restrict_rel_domain ((R (-> $$unsorted $$unsorted Bool)) (S (-> $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (and (@ S X) (@ (@ R X) Y))) % 0.15/0.35 (define-fun tptp.rel_diagonal ((X $$unsorted) (Y $$unsorted)) Bool (= X Y)) % 0.15/0.35 (define-fun tptp.rel_composition ((R1 (-> $$unsorted $$unsorted Bool)) (R2 (-> $$unsorted $$unsorted Bool)) (X $$unsorted) (Z $$unsorted)) Bool (not (forall ((Y $$unsorted)) (or (not (R1 X Y)) (not (R2 Y Z)))))) % 0.15/0.35 (define-fun tptp.reflexive ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted)) (R X X))) % 0.15/0.35 (define-fun tptp.irreflexive ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted)) (not (R X X)))) % 0.15/0.35 (define-fun tptp.symmetric ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (R Y X)))) % 0.15/0.35 (define-fun tptp.transitive ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (R X Y)) (not (R Y Z)) (R X Z)))) % 0.15/0.35 (define-fun tptp.equiv_rel ((R (-> $$unsorted $$unsorted Bool))) Bool (and (forall ((X $$unsorted)) (R X X)) (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (R Y X))) (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (R X Y)) (not (R Y Z)) (R X Z))))) % 0.15/0.35 (define-fun tptp.rel_codomain ((R (-> $$unsorted $$unsorted Bool)) (Y $$unsorted)) Bool (not (forall ((X $$unsorted)) (not (R X Y))))) % 0.15/0.35 (define-fun tptp.rel_domain ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted)) Bool (not (forall ((Y $$unsorted)) (not (R X Y))))) % 0.15/0.35 (define-fun tptp.rel_inverse ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (@ (@ R Y) X)) % 0.15/0.35 (define-fun tptp.equiv_classes ((R (-> $$unsorted $$unsorted Bool)) (S1 (-> $$unsorted Bool))) Bool (not (forall ((X $$unsorted)) (or (not (S1 X)) (not (forall ((Y $$unsorted)) (= (R X Y) (S1 Y)))))))) % 0.15/0.35 (define-fun tptp.restrict_rel_codomain ((R (-> $$unsorted $$unsorted Bool)) (S (-> $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (and (@ S Y) (@ (@ R X) Y))) % 0.15/0.35 (define-fun tptp.rel_field ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted)) Bool (or (not (forall ((Y $$unsorted)) (not (R X Y)))) (not (forall ((BOUND_VARIABLE_920 $$unsorted)) (not (R BOUND_VARIABLE_920 X)))))) % 0.15/0.35 (define-fun tptp.well_founded ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X (-> $$unsorted Bool)) (Z $$unsorted)) (or (not (X Z)) (not (forall ((Y $$unsorted)) (or (not (X Y)) (not (forall ((W $$unsorted)) (or (not (R Y W)) (not (X W))))))))))) % 0.15/0.35 (define-fun tptp.upwards_well_founded ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X (-> $$unsorted Bool)) (Z $$unsorted)) (or (not (X Z)) (not (forall ((Y $$unsorted)) (or (not (X Y)) (and (R Y Y) (not (forall ((W $$unsorted)) (not (X W))))))))))) % 0.15/0.35 ) % 0.15/0.35 % SZS output end Model % 0.15/0.36 % cvc5 exiting %------------------------------------------------------------------------------