diff --git a/redex-doc/redex/scribblings/ref/testing.scrbl b/redex-doc/redex/scribblings/ref/testing.scrbl
index 41d57aad..c8cca86f 100644
--- a/redex-doc/redex/scribblings/ref/testing.scrbl
+++ b/redex-doc/redex/scribblings/ref/testing.scrbl
@@ -153,11 +153,51 @@ relation @racket[rel-expr] to a term specified by @racket[goal-expr] in
        
        (test-results)]
 
-@defform*[((test-judgment-holds (judgment-form-or-relation pat/term ...))
-           (test-judgment-holds modeless-judgment-form derivation-expr))]{
+@defform*/subs[((test-judgment-holds (judgment-form-or-relation pat/term ...) mutuals)
+                (test-judgment-holds modeless-judgment-form derivation-expr))
+                ([mutuals (code:line)
+                          (code:line #:mutuals (judgment-form-id ...))])]{
  In the first form, tests to see if @racket[(judgment-form-or-relation pat/term ...)] holds.
  In the second form, tests to see if the result of @racket[derivation-expr] is a derivation and,
  if so, that it is derivable using @racket[modeless-judgment-form].
+
+ For modeless judgments, if the derivation is invalid, the test will report the
+ all the proper sub-derivations of @racket[modeless-judgment-form] that fail to hold.
+ If @racket[modeless-judgment-form] has other judgment premises, these
+ identifiers can be supplied in the optional #racket[#:mutuals] arguments, and
+ the form will report each invalid sub-derivations from all the specified judgment forms.
+
+@examples[
+#:eval redex-eval
+(define-language L)
+(define-judgment-form L
+  [----------- "Base"
+   (J1 natural 1)])
+
+(define-judgment-form L
+  [----------- "Base"
+   (J2 natural 1)]
+
+  [(J1 any_1 any_2)
+   (J2 any_1 any_3)
+   -------------- "Pair"
+   (J2 (any_1 any_2) any_3)])
+
+(test-judgment-holds J2 (derivation `(J2 (1 x) 1) "Pair"
+                                    (list
+                                     (derivation `(J1 1 x) "Base"
+                                                 (list))
+                                     (derivation `(J2 1 1) "Base"
+                                                 (list)))))
+
+(test-judgment-holds J2 (derivation `(J2 (1 x) 1) "Pair"
+                                    (list
+                                     (derivation `(J1 1 x) "Base"
+                                                 (list))
+                                     (derivation `(J2 1 1) "Base"
+                                                 (list))))
+                     #:mutuals (J1))
+]
 }
 
 @defform[(test-predicate p? e)]{
diff --git a/redex-lib/redex/private/modeless-jf.rkt b/redex-lib/redex/private/modeless-jf.rkt
index 4a40a84e..b8a78a18 100644
--- a/redex-lib/redex/private/modeless-jf.rkt
+++ b/redex-lib/redex/private/modeless-jf.rkt
@@ -245,9 +245,13 @@
 ;;                              hash[rulename -o> (listof modeless-jf-clause?)]
 ;;                              compiled-pattern
 ;;                              derivation
-;;                           -> match or #f
+;;                              boolean
+;;                              fail: (list/c derivation?) -> any/c
+;;                           -> #t or any/c
+;; a list of derivations indicates the list of sub-derivations that did not match.
 (define (call-modeless-judgment-form lang jf-name modeless-jf-clause-table contract-cp deriv
-                                     only-check-contracts?)
+                                     only-check-contracts?
+                                     [fail (λ _ #f)])
   (match deriv
     [(derivation (cons deriv-jf-name jf-args) rule-name sub-derivations)
      (cond
@@ -262,7 +266,7 @@
               rules
               jf-args
               sub-derivations
-              (λ () #f))]
+              fail)]
             [else
              (define known-rules (sort (hash-keys modeless-jf-clause-table) string<?))
              (error jf-name "unknown rule in derivation\n  rule: ~.s\n  known rules:~a"
@@ -270,8 +274,8 @@
                     (apply string-append
                            (for/list ([rule (in-list known-rules)])
                              (format "\n   ~s" rule))))]))]
-       [else #f])]
-    [_ #f]))
+       [else (fail (list deriv))])]
+    [_ (fail (list deriv))]))
 
 (define (modeless-judgment-form-check-contract jf-name contract-cp jf-args)
   (when contract-cp
@@ -300,9 +304,9 @@
               first-set-of-args
               maybe-more-args)))))
 
-(define (modeless-jf-process-rule-candidates lang candidates jf-args sub-derivations fail)
+(define (modeless-jf-process-rule-candidates lang candidates jf-args sub-derivations fail [bad-derivs '()])
   (match candidates
-    [`() (fail)]
+    [`() (fail bad-derivs)]
     [(cons (modeless-jf-clause conclusion-compiled-pattern
                                conclusion-ids-to-duplicate
                                premises-compiled-pattern
@@ -313,12 +317,13 @@
                                premise-jf-procs)
            more-candidates)
      (define conc-mtch (match-pattern conclusion-compiled-pattern jf-args))
-     (define (fail-to-next-candidate)
+     (define (fail-to-next-candidate bad-subderivs)
        (modeless-jf-process-rule-candidates lang
                                             more-candidates
                                             jf-args
                                             sub-derivations
-                                            fail))
+                                            fail
+                                            (append bad-subderivs bad-derivs)))
      (cond
        [conc-mtch
         (define sub-derivations-arguments-term-list
@@ -363,9 +368,10 @@
                                                   (mtch-bindings sub-derivations-mtch)
                                                   premises-repeat-names
                                                   premise-jf-procs
-                                                  #t)))
-           (fail-to-next-candidate)])]
-       [else (fail-to-next-candidate)])]))
+                                                  #t
+                                                  (λ _ #f))))
+           (fail-to-next-candidate sub-derivations)])]
+       [else (fail-to-next-candidate '())])]))
 
 
 (define (modeless-jf-process-other-conditions lang
@@ -376,16 +382,19 @@
                                               premise-jf-procs
                                               fail)
   (match conc+sub-bindings
-    [`() (fail)]
+    [`() (fail sub-derivations)]
     [(cons conc+sub-binding conc+sub-bindings)
      (cond
        [(and (not-failure-value? (other-conditions conc+sub-binding))
-             (modeless-jf-check-sub-derivations lang
-                                                sub-derivations
-                                                conc+sub-binding
-                                                premises-repeat-names
-                                                premise-jf-procs
-                                                #f))
+             ; BLEH
+             (equal? #t
+                     (modeless-jf-check-sub-derivations lang
+                                                        sub-derivations
+                                                        conc+sub-binding
+                                                        premises-repeat-names
+                                                        premise-jf-procs
+                                                        #f
+                                                        fail)))
         #t]
        [else
         (modeless-jf-process-other-conditions lang
@@ -406,7 +415,8 @@
                                            conc+sub-binding
                                            premises-repeat-names
                                            premise-jf-procs
-                                           contract-checking-only?)
+                                           contract-checking-only?
+                                           fail)
   (let loop ([premise-jf-procs premise-jf-procs]
              [premises-repeat-names premises-repeat-names]
              [sub-derivations sub-derivations])
@@ -430,8 +440,8 @@
                (cond
                  [(premise-jf-proc sub-derivation contract-checking-only?)
                   (n-loop (- n 1) sub-derivations)]
-                 [else #f])]
-              [_ #f])]))])))
+                 [else (fail (list sub-derivation))])]
+              [_ (fail (list sub-derivations))])]))])))
 
 (struct modeless-jf-clause (conclusion-compiled-pattern
                             conclusion-ids-to-duplicate
diff --git a/redex-lib/redex/private/reduction-semantics.rkt b/redex-lib/redex/private/reduction-semantics.rkt
index 5f1b888c..f4e1828e 100644
--- a/redex-lib/redex/private/reduction-semantics.rkt
+++ b/redex-lib/redex/private/reduction-semantics.rkt
@@ -8,6 +8,7 @@
          "loc-wrapper.rkt"
          "error.rkt"
          "judgment-form.rkt"
+         "modeless-jf.rkt"
          "search.rkt"
          "enum.rkt"
          (only-in "binding-forms.rkt"
@@ -3060,7 +3061,8 @@
 
 (define-syntax (test-judgment-holds stx)
   (syntax-parse stx
-    [(_ jf e:expr)
+    [(_ jf e:expr (~optional (~seq #:mutuals (mjf:id ...))
+                             #:defaults ([(mjf 1) '()])))
      (unless (judgment-form-id? #'jf)
        (raise-syntax-error 'test-judgment-holds
                            "expected a modeless judgment-form"
@@ -3071,8 +3073,19 @@
        (raise-syntax-error 'test-judgment-holds
                            "expected a modeless judgment-form"
                            #'jf))
+     (define judgment-form-record (lookup-judgment-form-id #'jf))
      #`(let ([derivation e])
-         (test-modeless-jf/proc 'jf (lambda (x) (judgment-holds jf x)) derivation (judgment-holds jf derivation) #,(get-srcloc stx)))]
+         (test-modeless-jf/proc 'jf derivation
+                                ; Circumvents some of the error checking and judgment tracing of judgment-holds
+                                (call-modeless-judgment-form #,(judgment-form-lang judgment-form-record)
+                                                             'jf
+                                                             #,(judgment-form-proc judgment-form-record)
+                                                             #,(judgment-form-compiled-input-contract-pat-id
+                                                                judgment-form-record)
+                                                             derivation
+                                                             #f
+                                                             values)
+                                #,(get-srcloc stx)))]
     [(_ (jf . rest))
      (unless (judgment-form-id? #'jf)
        (raise-syntax-error 'test-judgment-holds
@@ -3152,21 +3165,15 @@
        (newline op)
        0])))
 
-(define (print-failing-subderivations f d)
-  (define (print-derivation-error d)
-    (parameterize ([pretty-print-print-line (derivation-pretty-printer "    ")])
-      (pretty-print d (current-error-port))))
-  (let loop ([d d])
-    (let ([ls (derivation-subs d)])
-      (for ([d ls])
-        (unless (loop d)
-          (print-derivation-error d)))
-      (unless (f d)
-        (print-derivation-error d)))))
-
-(define (test-modeless-jf/proc jf jf-pred derivation val srcinfo)
+
+(define (print-failing-subderivations bad-sub-derivations)
+  (parameterize ([pretty-print-print-line (derivation-pretty-printer "    ")])
+    (for ([d (remove-duplicates bad-sub-derivations)])
+      (pretty-print d (current-error-port)))))
+
+(define (test-modeless-jf/proc jf derivation val srcinfo)
   (cond
-    [val
+    [(equal? #t val)
      (inc-successes)]
     [else
      (inc-failures)
@@ -3174,9 +3181,10 @@
      (eprintf "  derivation does not satisfy ~a\n" jf)
      (parameterize ([pretty-print-print-line (derivation-pretty-printer "  ")])
        (pretty-print derivation (current-error-port)))
-     (when (not (null? (derivation-subs derivation)))
+     ; A list indicates a list of bad sub-derivations
+     (when (and val (not (null? val)))
        (eprintf"  because the following sub-derivations fail:\n")
-       (print-failing-subderivations jf-pred derivation))]))
+       (print-failing-subderivations val))]))
 
 (define (test-judgment-holds/proc thunk name lang pat srcinfo is-relation?)
   (define results (thunk))
diff --git a/redex-test/redex/tests/tl-test.rkt b/redex-test/redex/tests/tl-test.rkt
index 8d6aef4e..c87e6161 100644
--- a/redex-test/redex/tests/tl-test.rkt
+++ b/redex-test/redex/tests/tl-test.rkt
@@ -199,14 +199,14 @@
     (test-judgment-holds J (derivation `(J (x 0) 0) "Pair"
                                        (list
                                         (derivation `(J x 0) "Base" (list))))))
-   (regexp (regexp-quote "because the following sub-derivations fail:\n    (derivation '(J x 0) \"Base\" '())\n    (derivation '(J (x 0) 0) \"Pair\" (list (derivation '(J x 0) \"Base\" '())))\n")))
+   (regexp (regexp-quote "because the following sub-derivations fail:\n    (derivation '(J x 0) \"Base\" '())")))
 
   (test
    (capture-output
     (test-judgment-holds J (derivation `(J (1 x) 0) "Pair"
                                        (list
                                         (derivation `(J 1 0) "Base" (list))))))
-   (regexp (regexp-quote "because the following sub-derivations fail:\n    (derivation '(J 1 0) \"Base\" '())\n    (derivation '(J (1 x) 0) \"Pair\" (list (derivation '(J 1 0) \"Base\" '())))\n")))
+   (regexp (regexp-quote "because the following sub-derivations fail:\n    (derivation '(J 1 0) \"Base\" '())")))
 
   (test
    (capture-output
@@ -226,6 +226,69 @@
   (test (capture-output (test-results))
         "3 tests failed (out of 4 total).\n"))
 
+(let ()
+  (define-judgment-form empty-language
+    [----------- "Base"
+     (J1 natural 1)])
+
+  (define-judgment-form empty-language
+    [----------- "Base"
+     (J2 natural 1)]
+
+    [(J1 any_1 any_2)
+     (J2 any_1 any_3)
+     -------------- "Pair"
+     (J2 (any_1 any_2) any_3)])
+
+  (test
+   (capture-output
+    (test-judgment-holds J2 (derivation `(J2 (1 x) 1) "Pair"
+                                        (list
+                                         (derivation `(J1 1 x) "Base"
+                                                     (list))
+                                         (derivation `(J2 1 1) "Base"
+                                                     (list))))))
+   (regexp
+    (regexp-quote "because the following sub-derivations fail:
+    (derivation '(J1 1 x) \"Base\" '())")))
+
+  (test
+   (capture-output
+    (test-judgment-holds J2 (derivation `(J2 (1 x) 1) "Pair"
+                                        (list
+                                         (derivation `(J1 1 x) "Base"
+                                                     (list))
+                                         (derivation `(J2 1 1) "Base"
+                                                     (list))))))
+   (regexp
+    (regexp-quote "because the following sub-derivations fail:
+    (derivation '(J1 1 x) \"Base\" '())")))
+
+  (test
+   (capture-output
+    (test-judgment-holds J2 (derivation `(J2 (1 1) 2) "Pair"
+                                        (list
+                                         (derivation `(J1 1 1) "Base"
+                                                     (list))
+                                         (derivation `(J2 1 2) "Base"
+                                                     (list))))))
+   (regexp
+    (regexp-quote "because the following sub-derivations fail:
+    (derivation '(J2 1 2) \"Base\" '())")))
+
+  (test
+   (capture-output
+    (test-judgment-holds J2 (derivation `(J2 (2 1) 1) "Pair"
+                                        (list
+                                         (derivation `(J1 2 1) "Base"
+                                                     (list))
+                                         (derivation `(J2 2 1) "Base"
+                                                     (list))))))
+   "")
+
+  (test (capture-output (test-results))
+        "3 tests failed (out of 4 total).\n"))
+
 (let ()
   (define-judgment-form empty-language
     #:mode (broken-swap I I O O)