%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : SEV441^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 : n015.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.38s 0.58s % Output : Model 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV441^1 : TPTP v9.2.1. Released v6.4.0. % 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.17/0.34 % Computer : n015.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 18:33:04 EDT 2026 % 0.17/0.35 % CPUTime : % 0.28/0.50 %----Disproving TH0 % 0.28/0.52 --- 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.38/0.58 % SZS status Satisfiable % 0.38/0.58 % SZS output start Model % 0.38/0.58 ( % 0.38/0.58 ; cardinality of $$unsorted is 1 % 0.38/0.58 ; rep: (as @$$unsorted_0 $$unsorted) % 0.38/0.58 (define-fun tptp.subrel ((R (-> $$unsorted $$unsorted Bool)) (S (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (S X Y)))) % 0.38/0.58 (define-fun tptp.inv ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (@ (@ R Y) X)) % 0.38/0.58 (define-fun tptp.idem ((F (-> (-> $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool))) Bool (forall ((R (-> $$unsorted $$unsorted Bool))) (= (@ F R) (@ F (@ F R))))) % 0.38/0.58 (define-fun tptp.infl ((F (-> (-> $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool))) Bool (forall ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (F R X Y)))) % 0.38/0.58 (define-fun tptp.mono ((F (-> (-> $$unsorted $$unsorted Bool) $$unsorted $$unsorted Bool))) Bool (forall ((R (-> $$unsorted $$unsorted Bool)) (S (-> $$unsorted $$unsorted Bool)) (BOUND_VARIABLE_508 $$unsorted) (BOUND_VARIABLE_510 $$unsorted)) (or (not (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (S X Y)))) (not (F R BOUND_VARIABLE_508 BOUND_VARIABLE_510)) (F S BOUND_VARIABLE_508 BOUND_VARIABLE_510)))) % 0.38/0.58 (define-fun tptp.refl ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted)) (R X X))) % 0.38/0.58 (define-fun tptp.irrefl ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted)) (not (R X X)))) % 0.38/0.58 (define-fun tptp.rc ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (or (= X Y) (@ (@ R X) Y))) % 0.38/0.58 (define-fun tptp.symm ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (R Y X)))) % 0.38/0.58 (define-fun tptp.antisymm ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (not (R Y X)) (= X Y)))) % 0.38/0.58 (define-fun tptp.asymm ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (not (R Y X))))) % 0.38/0.58 (define-fun tptp.sc ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (or (@ (@ R Y) X) (@ (@ R X) Y))) % 0.38/0.58 (define-fun tptp.trans ((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.38/0.58 (define-fun tptp.tc ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (Z $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 Z)) (S BOUND_VARIABLE_670 Z)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X Y)))) % 0.38/0.58 (define-fun tptp.trc ((R (-> $$unsorted $$unsorted Bool)) (__flatten_var_0 $$unsorted) (__flatten_var_1 $$unsorted)) Bool (or (= __flatten_var_0 __flatten_var_1) (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (Z $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 Z)) (S BOUND_VARIABLE_670 Z)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S __flatten_var_0 __flatten_var_1))))) % 0.38/0.58 (define-fun tptp.trsc ((R (-> $$unsorted $$unsorted Bool)) (__flatten_var_0 $$unsorted) (__flatten_var_1 $$unsorted)) Bool (or (= __flatten_var_0 __flatten_var_1) (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (Z $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 Z)) (S BOUND_VARIABLE_670 Z)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S __flatten_var_1 __flatten_var_0))) (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (Z $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 Z)) (S BOUND_VARIABLE_670 Z)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S __flatten_var_0 __flatten_var_1))))) % 0.38/0.58 (define-fun tptp.po ((R (-> $$unsorted $$unsorted Bool))) Bool (and (forall ((X $$unsorted)) (R X X)) (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (not (R Y X)) (= X Y))) (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (R X Y)) (not (R Y Z)) (R X Z))))) % 0.38/0.58 (define-fun tptp.so ((R (-> $$unsorted $$unsorted Bool))) Bool (and (forall ((X $$unsorted) (Y $$unsorted)) (or (not (R X Y)) (not (R Y X)))) (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (R X Y)) (not (R Y Z)) (R X Z))))) % 0.38/0.58 (define-fun tptp.total ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted)) (or (= X Y) (R X Y) (R Y X)))) % 0.38/0.58 (define-fun tptp.term ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((A (-> $$unsorted Bool)) (BOUND_VARIABLE_860 $$unsorted)) (or (not (A BOUND_VARIABLE_860)) (not (forall ((X $$unsorted)) (or (not (A X)) (not (forall ((Y $$unsorted)) (or (not (A Y)) (not (R X Y))))))))))) % 0.38/0.58 (define-fun tptp.ind ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((P (-> $$unsorted Bool)) (BOUND_VARIABLE_915 $$unsorted)) (or (not (forall ((X $$unsorted)) (or (not (forall ((Y $$unsorted)) (or (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (Z $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 Z)) (S BOUND_VARIABLE_670 Z)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X Y)))) (P Y)))) (P X)))) (P BOUND_VARIABLE_915)))) % 0.38/0.58 (define-fun tptp.innf ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted)) Bool (forall ((Y $$unsorted)) (not (R X Y)))) % 0.38/0.58 (define-fun tptp.nfof ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (and (or (= X Y) (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (Z $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 Z)) (S BOUND_VARIABLE_670 Z)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Y X)))) (forall ((BOUND_VARIABLE_983 $$unsorted)) (not (R X BOUND_VARIABLE_983))))) % 0.38/0.58 (define-fun tptp.norm ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (BOUND_VARIABLE_1073 $$unsorted)) (or (not (R X BOUND_VARIABLE_1073)) (not (forall ((BOUND_VARIABLE_1047 $$unsorted)) (or (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (Z $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 Z)) (S BOUND_VARIABLE_670 Z)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X BOUND_VARIABLE_1047)))) (not (forall ((BOUND_VARIABLE_983 $$unsorted)) (not (R BOUND_VARIABLE_1047 BOUND_VARIABLE_983)))))))))) % 0.38/0.58 (define-fun tptp.join ((R (-> $$unsorted $$unsorted Bool)) (X $$unsorted) (Y $$unsorted)) Bool (not (and (not (= X Y)) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Y X)))) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X Y)))) (forall ((BOUND_VARIABLE_1216 $$unsorted)) (or (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Y BOUND_VARIABLE_1216)))) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X BOUND_VARIABLE_1216))))))))) % 0.38/0.58 (define-fun tptp.lconfl ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted) (BOUND_VARIABLE_1291 (-> $$unsorted $$unsorted Bool)) (BOUND_VARIABLE_1307 (-> $$unsorted $$unsorted Bool))) (or (not (R X Z)) (not (R X Y)) (= Y Z) (not (forall ((BOUND_VARIABLE_1216 $$unsorted)) (or (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Y BOUND_VARIABLE_1216)))) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Z BOUND_VARIABLE_1216))))))) (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (BOUND_VARIABLE_1291 BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (BOUND_VARIABLE_1291 BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (BOUND_VARIABLE_1291 BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (BOUND_VARIABLE_1291 BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (BOUND_VARIABLE_1291 Y Z) (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (BOUND_VARIABLE_1307 BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (BOUND_VARIABLE_1307 BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (BOUND_VARIABLE_1307 BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (BOUND_VARIABLE_1307 BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (BOUND_VARIABLE_1307 Z Y)))) % 0.38/0.58 (define-fun tptp.sconfl ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted) (BOUND_VARIABLE_1369 (-> $$unsorted $$unsorted Bool)) (BOUND_VARIABLE_1385 (-> $$unsorted $$unsorted Bool))) (or (not (R X Z)) (and (not (= X Y)) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1345 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1345)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1345)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X Y))))) (= Y Z) (not (forall ((BOUND_VARIABLE_1216 $$unsorted)) (or (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Y BOUND_VARIABLE_1216)))) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Z BOUND_VARIABLE_1216))))))) (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (BOUND_VARIABLE_1369 BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (BOUND_VARIABLE_1369 BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (BOUND_VARIABLE_1369 BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (BOUND_VARIABLE_1369 BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (BOUND_VARIABLE_1369 Y Z) (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (BOUND_VARIABLE_1385 BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (BOUND_VARIABLE_1385 BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (BOUND_VARIABLE_1385 BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (BOUND_VARIABLE_1385 BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (BOUND_VARIABLE_1385 Z Y)))) % 0.38/0.58 (define-fun tptp.confl ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted) (BOUND_VARIABLE_1442 (-> $$unsorted $$unsorted Bool)) (BOUND_VARIABLE_1458 (-> $$unsorted $$unsorted Bool))) (or (and (not (= X Z)) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X Z))))) (and (not (= X Y)) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1420 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1420)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1420)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X Y))))) (= Y Z) (not (forall ((BOUND_VARIABLE_1216 $$unsorted)) (or (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Y BOUND_VARIABLE_1216)))) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Z BOUND_VARIABLE_1216))))))) (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (BOUND_VARIABLE_1442 BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (BOUND_VARIABLE_1442 BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (BOUND_VARIABLE_1442 BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (BOUND_VARIABLE_1442 BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (BOUND_VARIABLE_1442 Y Z) (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (BOUND_VARIABLE_1458 BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (BOUND_VARIABLE_1458 BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (BOUND_VARIABLE_1458 BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (BOUND_VARIABLE_1458 BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (BOUND_VARIABLE_1458 Z Y)))) % 0.38/0.58 (define-fun tptp.cr ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((X $$unsorted) (Y $$unsorted) (BOUND_VARIABLE_1520 (-> $$unsorted $$unsorted Bool)) (BOUND_VARIABLE_1536 (-> $$unsorted $$unsorted Bool))) (or (and (not (= X Y)) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (Z $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 Z)) (S BOUND_VARIABLE_670 Z)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Y X)))) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (Z $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 Z)) (S BOUND_VARIABLE_670 Z)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X Y))))) (= X Y) (not (forall ((BOUND_VARIABLE_1216 $$unsorted)) (or (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S Y BOUND_VARIABLE_1216)))) (not (forall ((S (-> $$unsorted $$unsorted Bool))) (or (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (S BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (S BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (S BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (S BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (S X BOUND_VARIABLE_1216))))))) (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1123 $$unsorted)) (or (not (BOUND_VARIABLE_1520 BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (BOUND_VARIABLE_1520 BOUND_VARIABLE_672 BOUND_VARIABLE_1123)) (BOUND_VARIABLE_1520 BOUND_VARIABLE_670 BOUND_VARIABLE_1123)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (BOUND_VARIABLE_1520 BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (BOUND_VARIABLE_1520 Y X) (not (forall ((BOUND_VARIABLE_670 $$unsorted) (BOUND_VARIABLE_672 $$unsorted) (BOUND_VARIABLE_1104 $$unsorted)) (or (not (BOUND_VARIABLE_1536 BOUND_VARIABLE_670 BOUND_VARIABLE_672)) (not (BOUND_VARIABLE_1536 BOUND_VARIABLE_672 BOUND_VARIABLE_1104)) (BOUND_VARIABLE_1536 BOUND_VARIABLE_670 BOUND_VARIABLE_1104)))) (not (forall ((BOUND_VARIABLE_659 $$unsorted) (BOUND_VARIABLE_661 $$unsorted)) (or (not (R BOUND_VARIABLE_659 BOUND_VARIABLE_661)) (BOUND_VARIABLE_1536 BOUND_VARIABLE_659 BOUND_VARIABLE_661)))) (BOUND_VARIABLE_1536 X Y)))) % 0.38/0.58 ) % 0.38/0.58 % SZS output end Model % 0.38/0.58 % cvc5 exiting %------------------------------------------------------------------------------