This file contains complete derivation details for Shan, Chung-chieh and Chris Barker. 2005. Explaining crossover and superiority as left-to-right evaluation. To appear in _Linguistics and Philosophy_. Also available (along with this file) at semanticsarchive.net This file contains complete details for each of the derivations discussed in the text. It should only be consulted if you can't get the parser to work; the parser code in standard Scheme should also be available at the semanticsarchive. With the parser, you can uncomment only the example you're interested in, as well as turn printing of the complete derivation on or off. #unspecified #unspecified #unspecified (Processing: (mary saw john)) ------------------- edge : 27 mary saw john (0 3) t semantics : ((saw j) m) proofnet : ((1 . t) (mary (2 . e)) (saw (((2 . e) \ (1 . t)) / (3 . e))) (john (3 . e))) derivation: (mary (saw john)) mary saw john t = ((saw j) m) mary e = m saw john (e \ t) = (saw j) saw ((e \ t) / e) = saw john e = j ------------------- edge : 102 mary saw john (0 3) t semantics : ((saw j) m) proofnet : ((1 . t) (mary (2 . e)) (saw (((2 . e) \ (3 . t)) / (4 . e))) (john (4 . e))) derivation: (D (U (mary (saw john)))) mary saw john t = ((saw j) m) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) mary saw john (1 // (t \\ 1)) = (^ f (f ((saw j) m))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mary saw john t = ((saw j) m) mary e = m saw john (e \ t) = (saw j) saw ((e \ t) / e) = saw john e = j 224 edges -- Done parsing. # (Processing: (john saw everyone)) ------------------- edge : 132 john saw everyone (0 3) t semantics : (forall x ((saw x) j)) proofnet : ((1 . t) (john (2 . e)) (saw (((2 . e) \ (3 . t)) / (4 . e))) (everyone ((1 . t) // ((4 . e) \\ (5 . t))))) derivation: (D ((S (U (L john))) ((S (U saw)) everyone))) john saw everyone t = (forall x ((saw x) j)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) john saw everyone (t // (t \\ t)) = (^ c (forall x (c ((saw x) j)))) john ((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (R (^ r (c (r j)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) john (1 // ((2 / (e \ 2)) \\ 1)) = (^ f (f (^ f (f j)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) john (1 / (e \ 1)) = (^ f (f j)) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) john e = j saw everyone (t // ((e \ t) \\ t)) = (^ c (forall x (c (saw x)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw everyone (t // (e \\ t)) = (^ k (forall x (k x))) ------------------- edge : 178 john saw everyone (0 3) t semantics : (forall x ((saw x) j)) proofnet : ((1 . t) (john (2 . e)) (saw (((2 . e) \ (3 . t)) / (4 . e))) (everyone ((5 . t) // ((4 . e) \\ (6 . t))))) derivation: (D (U (D ((S (U (L john))) ((S (U saw)) everyone))))) john saw everyone t = (forall x ((saw x) j)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) john saw everyone (1 // (t \\ 1)) = (^ f (f (forall x ((saw x) j)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) john saw everyone t = (forall x ((saw x) j)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) john saw everyone (t // (t \\ t)) = (^ c (forall x (c ((saw x) j)))) john ((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (R (^ r (c (r j)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) john (1 // ((2 / (e \ 2)) \\ 1)) = (^ f (f (^ f (f j)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) john (1 / (e \ 1)) = (^ f (f j)) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) john e = j saw everyone (t // ((e \ t) \\ t)) = (^ c (forall x (c (saw x)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw everyone (t // (e \\ t)) = (^ k (forall x (k x))) 303 edges -- Done parsing. # (Processing: (john mother left)) ------------------- edge : 27 john mother left (0 3) t semantics : (left (mother j)) proofnet : ((1 . t) (john (2 . e)) (mother ((2 . e) \ (3 . e))) (left ((3 . e) \ (1 . t)))) derivation: ((john mother) left) john mother left t = (left (mother j)) john mother e = (mother j) john e = j mother (e \ e) = mother left (e \ t) = left ------------------- edge : 99 john mother left (0 3) t semantics : (left (mother j)) proofnet : ((1 . t) (john (2 . e)) (mother ((2 . e) \ (3 . e))) (left ((3 . e) \ (4 . t)))) derivation: (D (U ((john mother) left))) john mother left t = (left (mother j)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) john mother left (1 // (t \\ 1)) = (^ f (f (left (mother j)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) john mother left t = (left (mother j)) john mother e = (mother j) john e = j mother (e \ e) = mother left (e \ t) = left 219 edges -- Done parsing. # (Processing: (everyone mother left)) ------------------- edge : 139 everyone mother left (0 3) t semantics : (forall x (left (mother x))) proofnet : ((1 . t) (everyone ((1 . t) // ((2 . e) \\ (3 . t)))) (mother ((2 . e) \ (4 . e))) (left ((4 . e) \ (5 . t)))) derivation: (D ((S ((S (U L)) ((S ((S (U L)) everyone)) (U mother)))) (U left))) everyone mother left t = (forall x (left (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) everyone mother left (t // (t \\ t)) = (^ c (forall x (c (left (mother x))))) everyone mother ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r (mother x)))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone mother (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f (mother x)))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone mother (t // (e \\ t)) = (^ c (forall x (c (mother x)))) everyone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 180 everyone mother left (0 3) t semantics : (forall x (left (mother x))) proofnet : ((1 . t) (everyone ((2 . t) // ((3 . e) \\ (4 . t)))) (mother ((3 . e) \ (5 . e))) (left ((5 . e) \ (6 . t)))) derivation: (D (U (D ((S ((S (U L)) ((S ((S (U L)) everyone)) (U mother)))) (U left))))) everyone mother left t = (forall x (left (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) everyone mother left (1 // (t \\ 1)) = (^ f (f (forall x (left (mother x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) everyone mother left t = (forall x (left (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) everyone mother left (t // (t \\ t)) = (^ c (forall x (c (left (mother x))))) everyone mother ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r (mother x)))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone mother (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f (mother x)))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone mother (t // (e \\ t)) = (^ c (forall x (c (mother x)))) everyone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left 305 edges -- Done parsing. # (Processing: (someone saw everyone)) ------------------- edge : 140 someone saw everyone (0 3) t semantics : (exists x (forall x1 ((saw x1) x))) proofnet : ((1 . t) (someone ((1 . t) // ((2 . e) \\ (3 . t)))) (saw (((2 . e) \ (4 . t)) / (5 . e))) (everyone ((3 . t) // ((5 . e) \\ (6 . t))))) derivation: (D ((S ((S (U L)) someone)) ((S (U saw)) everyone))) someone saw everyone t = (exists x (forall x1 ((saw x1) x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (t // (t \\ t)) = (^ c (exists x (forall x1 (c ((saw x1) x))))) someone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (exists x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) someone (t // ((1 / (e \ 1)) \\ t)) = (^ c (exists x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) someone (t // (e \\ t)) = (^ k (exists x (k x))) saw everyone (t // ((e \ t) \\ t)) = (^ c (forall x (c (saw x)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw everyone (t // (e \\ t)) = (^ k (forall x (k x))) ------------------- edge : 191 someone saw everyone (0 3) t semantics : (exists x (forall x1 ((saw x1) x))) proofnet : ((1 . t) (someone ((2 . t) // ((3 . e) \\ (4 . t)))) (saw (((3 . e) \ (5 . t)) / (6 . e))) (everyone ((4 . t) // ((6 . e) \\ (7 . t))))) derivation: (D (U (D ((S ((S (U L)) someone)) ((S (U saw)) everyone))))) someone saw everyone t = (exists x (forall x1 ((saw x1) x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (1 // (t \\ 1)) = (^ f (f (exists x (forall x1 ((saw x1) x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) someone saw everyone t = (exists x (forall x1 ((saw x1) x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (t // (t \\ t)) = (^ c (exists x (forall x1 (c ((saw x1) x))))) someone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (exists x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) someone (t // ((1 / (e \ 1)) \\ t)) = (^ c (exists x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) someone (t // (e \\ t)) = (^ k (exists x (k x))) saw everyone (t // ((e \ t) \\ t)) = (^ c (forall x (c (saw x)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw everyone (t // (e \\ t)) = (^ k (forall x (k x))) ------------------- edge : 201 someone saw everyone (0 3) t semantics : (exists x (forall x1 ((saw x1) x))) proofnet : ((1 . t) (someone ((1 . t) // ((2 . e) \\ (3 . t)))) (saw (((2 . e) \ (4 . t)) / (5 . e))) (everyone ((6 . t) // ((5 . e) \\ (7 . t))))) derivation: (D ((S (U D)) ((S ((S (U S)) ((S (U U)) ((S (U L)) someone)))) (U ((S (U saw)) everyone))))) someone saw everyone t = (exists x (forall x1 ((saw x1) x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (t // (t \\ t)) = (^ c (exists x (c (forall x1 ((saw x1) x))))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (t // ((t // (t \\ t)) \\ t)) = (^ c (exists x (c (^ c (forall x1 (c ((saw x1) x))))))) someone ((t // ((1 // (2 \\ 3)) \\ 4)) / (t // ((1 // ((e \ 2) \\ 3)) \\ 4))) = (^ R (^ c (exists x (R (^ r (c (^ c (r (^ r (c (r x))))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) someone (t // (((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) \\ t)) = (^ c (exists x (c (^ R (^ c (R (^ r (c (r x))))))))) RULE ((1 // (((2 // (3 \\ 4)) / (5 // (6 \\ 4))) \\ 7)) / (1 // ((2 // ((3 / 6) \\ 5)) \\ 7))) = (^ R (^ c (R (^ r (c (^ R (^ c (r (^ l (R (^ r (c (l r))))))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((((2 // (3 \\ 4)) / (5 // (6 \\ 4))) / (2 // ((3 / 6) \\ 5))) \\ 1)) = (^ f (f (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) someone (t // ((1 // ((2 / (e \ 2)) \\ 1)) \\ t)) = (^ c (exists x (c (^ f (f (^ f (f x))))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) someone (t // ((1 / (e \ 1)) \\ t)) = (^ c (exists x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) someone (t // (e \\ t)) = (^ k (exists x (k x))) saw everyone (1 // ((t // ((e \ t) \\ t)) \\ 1)) = (^ f (f (^ c (forall x (c (saw x)))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw everyone (t // ((e \ t) \\ t)) = (^ c (forall x (c (saw x)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw everyone (t // (e \\ t)) = (^ k (forall x (k x))) ------------------- edge : 209 someone saw everyone (0 3) t semantics : (forall x (exists x1 ((saw x) x1))) proofnet : ((1 . t) (someone ((2 . t) // ((3 . e) \\ (4 . t)))) (saw (((3 . e) \ (5 . t)) / (6 . e))) (everyone ((1 . t) // ((6 . e) \\ (7 . t))))) derivation: (D ((S (U D)) ((S (U (S ((S (U L)) someone)))) ((S (U U)) ((S (U saw)) everyone))))) someone saw everyone t = (forall x (exists x1 ((saw x) x1))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (t // (t \\ t)) = (^ c (forall x (c (exists x1 ((saw x) x1))))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (t // ((t // (t \\ t)) \\ t)) = (^ c (forall x (c (^ c (exists x1 (c ((saw x) x1))))))) someone ((1 // ((t // (2 \\ 3)) \\ 4)) / (1 // ((t // ((e \ 2) \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (exists x (r (^ r (c (r x))))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) someone (1 // (((t // (2 \\ 3)) / (t // ((e \ 2) \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (exists x (R (^ r (c (r x))))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) someone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (exists x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) someone (t // ((1 / (e \ 1)) \\ t)) = (^ c (exists x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) someone (t // (e \\ t)) = (^ k (exists x (k x))) saw everyone (t // ((1 // ((e \ t) \\ 1)) \\ t)) = (^ c (forall x (c (^ f (f (saw x)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw everyone (t // ((e \ t) \\ t)) = (^ c (forall x (c (saw x)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw everyone (t // (e \\ t)) = (^ k (forall x (k x))) ------------------- edge : 341 someone saw everyone (0 3) t semantics : (exists x (forall x1 ((saw x1) x))) proofnet : ((1 . t) (someone ((2 . t) // ((3 . e) \\ (4 . t)))) (saw (((3 . e) \ (5 . t)) / (6 . e))) (everyone ((7 . t) // ((6 . e) \\ (8 . t))))) derivation: (D (U (D ((S (U D)) ((S ((S (U S)) ((S (U U)) ((S (U L)) someone)))) (U ((S (U saw)) everyone))))))) someone saw everyone t = (exists x (forall x1 ((saw x1) x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (1 // (t \\ 1)) = (^ f (f (exists x (forall x1 ((saw x1) x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) someone saw everyone t = (exists x (forall x1 ((saw x1) x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (t // (t \\ t)) = (^ c (exists x (c (forall x1 ((saw x1) x))))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) someone saw everyone (t // ((t // (t \\ t)) \\ t)) = (^ c (exists x (c (^ c (forall x1 (c ((saw x1) x))))))) someone ((t // ((1 // (2 \\ 3)) \\ 4)) / (t // ((1 // ((e \ 2) \\ 3)) \\ 4))) = (^ R (^ c (exists x (R (^ r (c (^ c (r (^ r (c (r x))))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) someone (t // (((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) \\ t)) = (^ c (exists x (c (^ R (^ c (R (^ r (c (r x))))))))) RULE ((1 // (((2 // (3 \\ 4)) / (5 // (6 \\ 4))) \\ 7)) / (1 // ((2 // ((3 / 6) \\ 5)) \\ 7))) = (^ R (^ c (R (^ r (c (^ R (^ c (r (^ l (R (^ r (c (l r))))))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((((2 // (3 \\ 4)) / (5 // (6 \\ 4))) / (2 // ((3 / 6) \\ 5))) \\ 1)) = (^ f (f (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) someone (t // ((1 // ((2 / (e \ 2)) \\ 1)) \\ t)) = (^ c (exists x (c (^ f (f (^ f (f x))))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) someone (t // ((1 / (e \ 1)) \\ t)) = (^ c (exists x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) someone (t // (e \\ t)) = (^ k (exists x (k x))) saw everyone (1 // ((t // ((e \ t) \\ t)) \\ 1)) = (^ f (f (^ c (forall x (c (saw x)))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw everyone (t // ((e \ t) \\ t)) = (^ c (forall x (c (saw x)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw everyone (t // (e \\ t)) = (^ k (forall x (k x))) 613 edges -- Done parsing. # ((1 // ((t // (e \\ t)) \\ 1)) (^ f (f (^ k (forall x (k x)))))) ((t // ((1 // (e \\ 1)) \\ t)) (^ c (forall x (c (^ f (f x)))))) (t (forall x (exists x1 ((saw x) x1)))) (t (exists x (forall x1 ((saw x1) x)))) ((t // ((e > t) \\ (e > t))) (^ c (forall x ((c (^ r1 ((saw x) (mother r1)))) x)))) (((e \\ 1) // ((e ? t) \\ 1)) (^ c (^ r (c (^ r1 (((give r1) r) m)))))) #unspecified (Processing: (he left)) ------------------- edge : 85 he left (0 2) (e > t) semantics : (^ r (left r)) proofnet : (((1 . e) > (2 . t)) (he (((1 . e) > (2 . t)) // ((3 . e) \\ (2 . t)))) (left ((3 . e) \ (4 . t)))) derivation: (D ((S ((S (U L)) he)) (U left))) he left (e > t) = (^ r (left r)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left 181 edges -- Done parsing. # (Processing: (john saw him)) ------------------- edge : 132 john saw him (0 3) (e > t) semantics : (^ r ((saw r) j)) proofnet : (((1 . e) > (2 . t)) (john (3 . e)) (saw (((3 . e) \ (4 . t)) / (5 . e))) (him (((1 . e) > (2 . t)) // ((5 . e) \\ (2 . t))))) derivation: (D ((S (U (L john))) ((S (U saw)) him))) john saw him (e > t) = (^ r ((saw r) j)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) john saw him ((e > 1) // (t \\ 1)) = (^ c (^ r (c ((saw r) j)))) john ((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (R (^ r (c (r j)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) john (1 // ((2 / (e \ 2)) \\ 1)) = (^ f (f (^ f (f j)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) john (1 / (e \ 1)) = (^ f (f j)) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) john e = j saw him ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (saw r)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw him ((e > 1) // (e \\ 1)) = (^ k k) 236 edges -- Done parsing. # (Processing: (everyone saw him)) ------------------- edge : 159 everyone saw him (0 3) (e > t) semantics : (^ r (forall x ((saw r) x))) proofnet : (((1 . e) > (2 . t)) (everyone ((3 . t) // ((4 . e) \\ (5 . t)))) (saw (((4 . e) \ (6 . t)) / (7 . e))) (him (((1 . e) > (2 . t)) // ((7 . e) \\ (2 . t))))) derivation: (D ((S (U D)) ((S (U (S ((S (U L)) everyone)))) ((S (U U)) ((S (U saw)) him))))) everyone saw him (e > t) = (^ r (forall x ((saw r) x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) everyone saw him ((e > 1) // (t \\ 1)) = (^ c (^ r (c (forall x ((saw r) x))))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) everyone saw him ((e > 1) // ((t // (t \\ t)) \\ 1)) = (^ c (^ r (c (^ c (forall x (c ((saw r) x))))))) everyone ((1 // ((t // (2 \\ 3)) \\ 4)) / (1 // ((t // ((e \ 2) \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (forall x (r (^ r (c (r x))))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (1 // (((t // (2 \\ 3)) / (t // ((e \ 2) \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (forall x (R (^ r (c (r x))))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) everyone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) saw him ((e > 1) // ((2 // ((e \ t) \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (saw r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw him ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (saw r)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw him ((e > 1) // (e \\ 1)) = (^ k k) 264 edges -- Done parsing. # (Processing: (john thought he left)) ------------------- edge : 204 john thought he left (0 4) (e > t) semantics : (^ r ((thought (left r)) j)) proofnet : (((1 . e) > (2 . t)) (john (3 . e)) (thought (((3 . e) \ (4 . t)) / (5 . t))) (he (((1 . e) > (2 . t)) // ((6 . e) \\ (2 . t)))) (left ((6 . e) \ (5 . t)))) derivation: (D ((S (U (L john))) ((S (U thought)) ((S ((S (U L)) he)) (U left))))) john thought he left (e > t) = (^ r ((thought (left r)) j)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) john thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c ((thought (left r)) j)))) john ((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (R (^ r (c (r j)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) john (1 // ((2 / (e \ 2)) \\ 1)) = (^ f (f (^ f (f j)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) john (1 / (e \ 1)) = (^ f (f j)) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) john e = j thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 278 john thought he left (0 4) (e > t) semantics : (^ r ((thought (left r)) j)) proofnet : (((1 . e) > (2 . t)) (john (3 . e)) (thought (((3 . e) \ (4 . t)) / (5 . t))) (he (((1 . e) > (2 . t)) // ((6 . e) \\ (2 . t)))) (left ((6 . e) \ (7 . t)))) derivation: (D ((S (U (L john))) ((S (U thought)) ((S (U D)) ((S (U U)) ((S ((S (U L)) he)) (U left))))))) john thought he left (e > t) = (^ r ((thought (left r)) j)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) john thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c ((thought (left r)) j)))) john ((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (R (^ r (c (r j)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) john (1 // ((2 / (e \ 2)) \\ 1)) = (^ f (f (^ f (f j)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) john (1 / (e \ 1)) = (^ f (f j)) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) john e = j thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left 458 edges -- Done parsing. # ((t // (e \\ (e > t))) (^ d (forall x ((d x) x)))) (Processing: (B everyone thought he left)) ------------------- edge : 248 B everyone thought he left (0 5) t semantics : (forall x ((thought (left x)) x)) proofnet : ((1 . t) (B (((1 . t) // ((2 . e) \\ ((3 . e) > (4 . t)))) / ((1 . t) // ((5 . e) \\ (4 . t))))) (everyone ((1 . t) // ((5 . e) \\ (4 . t)))) (thought (((2 . e) \ (6 . t)) / (7 . t))) (he (((3 . e) > (4 . t)) // ((8 . e) \\ (4 . t)))) (left ((8 . e) \ (7 . t)))) derivation: (D ((S ((S (U L)) (B everyone))) ((S (U thought)) ((S ((S (U L)) he)) (U left))))) B everyone thought he left t = (forall x ((thought (left x)) x)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone thought he left (t // (t \\ t)) = (^ c (forall x (c ((thought (left x)) x)))) B everyone ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f x))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone (t // (e \\ (e > t))) = (^ d (forall x ((d x) x))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 341 B everyone thought he left (0 5) t semantics : (forall x ((thought (left x)) x)) proofnet : ((1 . t) (B (((1 . t) // ((2 . e) \\ ((3 . e) > (4 . t)))) / ((1 . t) // ((5 . e) \\ (4 . t))))) (everyone ((1 . t) // ((5 . e) \\ (4 . t)))) (thought (((2 . e) \ (6 . t)) / (7 . t))) (he (((3 . e) > (4 . t)) // ((8 . e) \\ (4 . t)))) (left ((8 . e) \ (9 . t)))) derivation: (D ((S ((S (U L)) (B everyone))) ((S (U thought)) ((S (U D)) ((S (U U)) ((S ((S (U L)) he)) (U left))))))) B everyone thought he left t = (forall x ((thought (left x)) x)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone thought he left (t // (t \\ t)) = (^ c (forall x (c ((thought (left x)) x)))) B everyone ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f x))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone (t // (e \\ (e > t))) = (^ d (forall x ((d x) x))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 371 B everyone thought he left (0 5) t semantics : (forall x ((thought (left x)) x)) proofnet : ((1 . t) (B (((2 . t) // ((3 . e) \\ ((4 . e) > (5 . t)))) / ((2 . t) // ((6 . e) \\ (5 . t))))) (everyone ((2 . t) // ((6 . e) \\ (5 . t)))) (thought (((3 . e) \ (7 . t)) / (8 . t))) (he (((4 . e) > (5 . t)) // ((9 . e) \\ (5 . t)))) (left ((9 . e) \ (8 . t)))) derivation: (D ((S (U D)) ((S (U (S ((S (U L)) (B everyone))))) ((S (U (S (U thought)))) (U ((S ((S (U L)) he)) (U left))))))) B everyone thought he left t = (forall x ((thought (left x)) x)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone thought he left (1 // (t \\ 1)) = (^ c (c (forall x ((thought (left x)) x)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone thought he left (1 // ((t // (t \\ t)) \\ 1)) = (^ c (c (^ c (forall x (c ((thought (left x)) x)))))) B everyone ((1 // ((t // (2 \\ 3)) \\ 4)) / (1 // (((e > t) // ((e \ 2) \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (forall x ((r (^ r (c (r x)))) x)))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (1 // (((t // (2 \\ 3)) / ((e > t) // ((e \ 2) \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) B everyone ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f x))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone (t // (e \\ (e > t))) = (^ d (forall x ((d x) x))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) thought he left (1 // (((e > 2) // ((e \ t) \\ 2)) \\ 1)) = (^ c (c (^ c (^ r (c (thought (left r))))))) thought ((1 // ((2 // ((e \ t) \\ 3)) \\ 4)) / (1 // ((2 // (t \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (r (^ r (c (thought r)))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((2 // ((e \ t) \\ 3)) / (2 // (t \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (R (^ r (c (thought r)))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left (1 // (((e > 2) // (t \\ 2)) \\ 1)) = (^ f (f (^ c (^ r (c (left r)))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 523 B everyone thought he left (0 5) t semantics : (forall x ((thought (left x)) x)) proofnet : ((1 . t) (B (((2 . t) // ((3 . e) \\ ((4 . e) > (5 . t)))) / ((2 . t) // ((6 . e) \\ (5 . t))))) (everyone ((2 . t) // ((6 . e) \\ (5 . t)))) (thought (((3 . e) \ (7 . t)) / (8 . t))) (he (((4 . e) > (5 . t)) // ((9 . e) \\ (5 . t)))) (left ((9 . e) \ (10 . t)))) derivation: (D ((S (U D)) ((S (U (S ((S (U L)) (B everyone))))) ((S (U (S (U thought)))) (U ((S (U D)) ((S (U U)) ((S ((S (U L)) he)) (U left))))))))) B everyone thought he left t = (forall x ((thought (left x)) x)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone thought he left (1 // (t \\ 1)) = (^ c (c (forall x ((thought (left x)) x)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone thought he left (1 // ((t // (t \\ t)) \\ 1)) = (^ c (c (^ c (forall x (c ((thought (left x)) x)))))) B everyone ((1 // ((t // (2 \\ 3)) \\ 4)) / (1 // (((e > t) // ((e \ 2) \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (forall x ((r (^ r (c (r x)))) x)))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (1 // (((t // (2 \\ 3)) / ((e > t) // ((e \ 2) \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) B everyone ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f x))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone (t // (e \\ (e > t))) = (^ d (forall x ((d x) x))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) thought he left (1 // (((e > 2) // ((e \ t) \\ 2)) \\ 1)) = (^ c (c (^ c (^ r (c (thought (left r))))))) thought ((1 // ((2 // ((e \ t) \\ 3)) \\ 4)) / (1 // ((2 // (t \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (r (^ r (c (thought r)))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((2 // ((e \ t) \\ 3)) / (2 // (t \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (R (^ r (c (thought r)))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left (1 // (((e > 2) // (t \\ 2)) \\ 1)) = (^ f (f (^ c (^ r (c (left r)))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left 922 edges -- Done parsing. # (Processing: (B everyone mother thought he left)) ------------------- edge : 341 B everyone mother thought he left (0 6) t semantics : (forall x ((thought (left x)) (mother x))) proofnet : ((1 . t) (B (((1 . t) // ((2 . e) \\ ((3 . e) > (4 . t)))) / ((1 . t) // ((5 . e) \\ (4 . t))))) (everyone ((1 . t) // ((5 . e) \\ (4 . t)))) (mother ((2 . e) \ (6 . e))) (thought (((6 . e) \ (7 . t)) / (8 . t))) (he (((3 . e) > (4 . t)) // ((9 . e) \\ (4 . t)))) (left ((9 . e) \ (8 . t)))) derivation: (D ((S ((S (U L)) ((S ((S (U L)) (B everyone))) (U mother)))) ((S (U thought)) ((S ((S (U L)) he)) (U left))))) B everyone mother thought he left t = (forall x ((thought (left x)) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (t // (t \\ t)) = (^ c (forall x (c ((thought (left x)) (mother x))))) B everyone mother ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r (mother x))))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone mother (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f (mother x)))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone mother (t // (e \\ (e > t))) = (^ c (forall x ((c (mother x)) x))) B everyone ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f x))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone (t // (e \\ (e > t))) = (^ d (forall x ((d x) x))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 441 B everyone mother thought he left (0 6) t semantics : (forall x ((thought (left x)) (mother x))) proofnet : ((1 . t) (B (((1 . t) // ((2 . e) \\ ((3 . e) > (4 . t)))) / ((1 . t) // ((5 . e) \\ (4 . t))))) (everyone ((1 . t) // ((5 . e) \\ (4 . t)))) (mother ((2 . e) \ (6 . e))) (thought (((6 . e) \ (7 . t)) / (8 . t))) (he (((3 . e) > (4 . t)) // ((9 . e) \\ (4 . t)))) (left ((9 . e) \ (10 . t)))) derivation: (D ((S ((S (U L)) ((S ((S (U L)) (B everyone))) (U mother)))) ((S (U thought)) ((S (U D)) ((S (U U)) ((S ((S (U L)) he)) (U left))))))) B everyone mother thought he left t = (forall x ((thought (left x)) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (t // (t \\ t)) = (^ c (forall x (c ((thought (left x)) (mother x))))) B everyone mother ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r (mother x))))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone mother (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f (mother x)))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone mother (t // (e \\ (e > t))) = (^ c (forall x ((c (mother x)) x))) B everyone ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f x))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone (t // (e \\ (e > t))) = (^ d (forall x ((d x) x))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 455 B everyone mother thought he left (0 6) t semantics : (forall x ((thought (left (mother x))) (mother x))) proofnet : ((1 . t) (B (((1 . t) // ((2 . e) \\ ((3 . e) > (4 . t)))) / ((1 . t) // ((5 . e) \\ (4 . t))))) (everyone ((1 . t) // ((6 . e) \\ (4 . t)))) (mother ((6 . e) \ (5 . e))) (thought (((2 . e) \ (7 . t)) / (8 . t))) (he (((3 . e) > (4 . t)) // ((9 . e) \\ (4 . t)))) (left ((9 . e) \ (10 . t)))) derivation: (D ((S ((S (U L)) (B ((S ((S (U L)) everyone)) (U mother))))) ((S (U thought)) ((S (U D)) ((S (U U)) ((S ((S (U L)) he)) (U left))))))) B everyone mother thought he left t = (forall x ((thought (left (mother x))) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (t // (t \\ t)) = (^ c (forall x (c ((thought (left (mother x))) (mother x))))) B everyone mother ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r (mother x))))) (mother x))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone mother (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f (mother x)))) (mother x)))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone mother (t // (e \\ (e > t))) = (^ d (forall x ((d (mother x)) (mother x)))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone mother (t // (e \\ t)) = (^ c (forall x (c (mother x)))) everyone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 460 B everyone mother thought he left (0 6) t semantics : (forall x ((thought (left (mother x))) (mother x))) proofnet : ((1 . t) (B (((1 . t) // ((2 . e) \\ ((3 . e) > (4 . t)))) / ((1 . t) // ((5 . e) \\ (4 . t))))) (everyone ((1 . t) // ((6 . e) \\ (4 . t)))) (mother ((6 . e) \ (5 . e))) (thought (((2 . e) \ (7 . t)) / (8 . t))) (he (((3 . e) > (4 . t)) // ((9 . e) \\ (4 . t)))) (left ((9 . e) \ (8 . t)))) derivation: (D ((S ((S (U L)) (B ((S ((S (U L)) everyone)) (U mother))))) ((S (U thought)) ((S ((S (U L)) he)) (U left))))) B everyone mother thought he left t = (forall x ((thought (left (mother x))) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (t // (t \\ t)) = (^ c (forall x (c ((thought (left (mother x))) (mother x))))) B everyone mother ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r (mother x))))) (mother x))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone mother (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f (mother x)))) (mother x)))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone mother (t // (e \\ (e > t))) = (^ d (forall x ((d (mother x)) (mother x)))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone mother (t // (e \\ t)) = (^ c (forall x (c (mother x)))) everyone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 486 B everyone mother thought he left (0 6) t semantics : (forall x ((thought (left x)) (mother x))) proofnet : ((1 . t) (B (((2 . t) // ((3 . e) \\ ((4 . e) > (5 . t)))) / ((2 . t) // ((6 . e) \\ (5 . t))))) (everyone ((2 . t) // ((6 . e) \\ (5 . t)))) (mother ((3 . e) \ (7 . e))) (thought (((7 . e) \ (8 . t)) / (9 . t))) (he (((4 . e) > (5 . t)) // ((10 . e) \\ (5 . t)))) (left ((10 . e) \ (9 . t)))) derivation: (D (U (D ((S ((S (U L)) ((S ((S (U L)) (B everyone))) (U mother)))) ((S (U thought)) ((S ((S (U L)) he)) (U left))))))) B everyone mother thought he left t = (forall x ((thought (left x)) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (1 // (t \\ 1)) = (^ f (f (forall x ((thought (left x)) (mother x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) B everyone mother thought he left t = (forall x ((thought (left x)) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (t // (t \\ t)) = (^ c (forall x (c ((thought (left x)) (mother x))))) B everyone mother ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r (mother x))))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone mother (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f (mother x)))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone mother (t // (e \\ (e > t))) = (^ c (forall x ((c (mother x)) x))) B everyone ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f x))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone (t // (e \\ (e > t))) = (^ d (forall x ((d x) x))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 640 B everyone mother thought he left (0 6) t semantics : (forall x ((thought (left x)) (mother x))) proofnet : ((1 . t) (B (((2 . t) // ((3 . e) \\ ((4 . e) > (5 . t)))) / ((2 . t) // ((6 . e) \\ (5 . t))))) (everyone ((2 . t) // ((6 . e) \\ (5 . t)))) (mother ((3 . e) \ (7 . e))) (thought (((7 . e) \ (8 . t)) / (9 . t))) (he (((4 . e) > (5 . t)) // ((10 . e) \\ (5 . t)))) (left ((10 . e) \ (11 . t)))) derivation: (D ((S (U D)) ((S (U (S ((S (U L)) ((S ((S (U L)) (B everyone))) (U mother)))))) ((S (U (S (U thought)))) (U ((S (U D)) ((S (U U)) ((S ((S (U L)) he)) (U left))))))))) B everyone mother thought he left t = (forall x ((thought (left x)) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (1 // (t \\ 1)) = (^ c (c (forall x ((thought (left x)) (mother x))))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (1 // ((t // (t \\ t)) \\ 1)) = (^ c (c (^ c (forall x (c ((thought (left x)) (mother x))))))) B everyone mother ((1 // ((t // (2 \\ 3)) \\ 4)) / (1 // (((e > t) // ((e \ 2) \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (forall x ((r (^ r (c (r (mother x))))) x)))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone mother (1 // (((t // (2 \\ 3)) / ((e > t) // ((e \ 2) \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (forall x ((R (^ r (c (r (mother x))))) x)))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) B everyone mother ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r (mother x))))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone mother (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f (mother x)))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone mother (t // (e \\ (e > t))) = (^ c (forall x ((c (mother x)) x))) B everyone ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r x)))) x)))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f x))) x))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone (t // (e \\ (e > t))) = (^ d (forall x ((d x) x))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother thought he left (1 // (((e > 2) // ((e \ t) \\ 2)) \\ 1)) = (^ c (c (^ c (^ r (c (thought (left r))))))) thought ((1 // ((2 // ((e \ t) \\ 3)) \\ 4)) / (1 // ((2 // (t \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (r (^ r (c (thought r)))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((2 // ((e \ t) \\ 3)) / (2 // (t \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (R (^ r (c (thought r)))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left (1 // (((e > 2) // (t \\ 2)) \\ 1)) = (^ f (f (^ c (^ r (c (left r)))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 718 B everyone mother thought he left (0 6) t semantics : (forall x ((thought (left (mother x))) (mother x))) proofnet : ((1 . t) (B (((2 . t) // ((3 . e) \\ ((4 . e) > (5 . t)))) / ((2 . t) // ((6 . e) \\ (5 . t))))) (everyone ((2 . t) // ((7 . e) \\ (5 . t)))) (mother ((7 . e) \ (6 . e))) (thought (((3 . e) \ (8 . t)) / (9 . t))) (he (((4 . e) > (5 . t)) // ((10 . e) \\ (5 . t)))) (left ((10 . e) \ (11 . t)))) derivation: (D (U (D ((S ((S (U L)) (B ((S ((S (U L)) everyone)) (U mother))))) ((S (U thought)) ((S (U D)) ((S (U U)) ((S ((S (U L)) he)) (U left))))))))) B everyone mother thought he left t = (forall x ((thought (left (mother x))) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (1 // (t \\ 1)) = (^ f (f (forall x ((thought (left (mother x))) (mother x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) B everyone mother thought he left t = (forall x ((thought (left (mother x))) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (t // (t \\ t)) = (^ c (forall x (c ((thought (left (mother x))) (mother x))))) B everyone mother ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r (mother x))))) (mother x))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone mother (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f (mother x)))) (mother x)))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone mother (t // (e \\ (e > t))) = (^ d (forall x ((d (mother x)) (mother x)))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone mother (t // (e \\ t)) = (^ c (forall x (c (mother x)))) everyone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 743 B everyone mother thought he left (0 6) t semantics : (forall x ((thought (left (mother x))) (mother x))) proofnet : ((1 . t) (B (((2 . t) // ((3 . e) \\ ((4 . e) > (5 . t)))) / ((2 . t) // ((6 . e) \\ (5 . t))))) (everyone ((2 . t) // ((7 . e) \\ (5 . t)))) (mother ((7 . e) \ (6 . e))) (thought (((3 . e) \ (8 . t)) / (9 . t))) (he (((4 . e) > (5 . t)) // ((10 . e) \\ (5 . t)))) (left ((10 . e) \ (9 . t)))) derivation: (D (U (D ((S ((S (U L)) (B ((S ((S (U L)) everyone)) (U mother))))) ((S (U thought)) ((S ((S (U L)) he)) (U left))))))) B everyone mother thought he left t = (forall x ((thought (left (mother x))) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (1 // (t \\ 1)) = (^ f (f (forall x ((thought (left (mother x))) (mother x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) B everyone mother thought he left t = (forall x ((thought (left (mother x))) (mother x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) B everyone mother thought he left (t // (t \\ t)) = (^ c (forall x (c ((thought (left (mother x))) (mother x))))) B everyone mother ((t // (1 \\ 2)) / ((e > t) // ((e \ 1) \\ 2))) = (^ R (^ c (forall x ((R (^ r (c (r (mother x))))) (mother x))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) B everyone mother (t // ((1 / (e \ 1)) \\ (e > t))) = (^ c (forall x ((c (^ f (f (mother x)))) (mother x)))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) B everyone mother (t // (e \\ (e > t))) = (^ d (forall x ((d (mother x)) (mother x)))) B ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))) = (^ c (^ d (c (^ x ((d x) x))))) everyone mother (t // (e \\ t)) = (^ c (forall x (c (mother x)))) everyone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother thought he left ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (thought (left r))))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left 1414 edges -- Done parsing. # (Processing: (everyone thought he left)) ------------------- edge : 267 everyone thought he left (0 4) (e > t) semantics : (^ r (forall x ((thought (left r)) x))) proofnet : (((1 . e) > (2 . t)) (everyone ((3 . t) // ((4 . e) \\ (5 . t)))) (thought (((4 . e) \ (6 . t)) / (7 . t))) (he (((1 . e) > (2 . t)) // ((8 . e) \\ (2 . t)))) (left ((8 . e) \ (7 . t)))) derivation: (D ((S (U D)) ((S (U (S ((S (U L)) everyone)))) ((S (U (S (U thought)))) ((S (U U)) ((S ((S (U L)) he)) (U left))))))) everyone thought he left (e > t) = (^ r (forall x ((thought (left r)) x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) everyone thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (forall x ((thought (left r)) x))))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) everyone thought he left ((e > 1) // ((t // (t \\ t)) \\ 1)) = (^ c (^ r (c (^ c (forall x (c ((thought (left r)) x))))))) everyone ((1 // ((t // (2 \\ 3)) \\ 4)) / (1 // ((t // ((e \ 2) \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (forall x (r (^ r (c (r x))))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (1 // (((t // (2 \\ 3)) / (t // ((e \ 2) \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (forall x (R (^ r (c (r x))))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) everyone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) thought he left ((e > 1) // ((2 // ((e \ t) \\ 2)) \\ 1)) = (^ c (^ r (c (^ c (c (thought (left r))))))) thought ((1 // ((2 // ((e \ t) \\ 3)) \\ 4)) / (1 // ((2 // (t \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (r (^ r (c (thought r)))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((2 // ((e \ t) \\ 3)) / (2 // (t \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (R (^ r (c (thought r)))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left ------------------- edge : 325 everyone thought he left (0 4) (e > t) semantics : (^ r (forall x ((thought (left r)) x))) proofnet : (((1 . e) > (2 . t)) (everyone ((3 . t) // ((4 . e) \\ (5 . t)))) (thought (((4 . e) \ (6 . t)) / (7 . t))) (he (((1 . e) > (2 . t)) // ((8 . e) \\ (2 . t)))) (left ((8 . e) \ (9 . t)))) derivation: (D ((S (U D)) ((S (U (S ((S (U L)) everyone)))) ((S (U (S (U thought)))) ((S (U U)) ((S (U D)) ((S (U U)) ((S ((S (U L)) he)) (U left))))))))) everyone thought he left (e > t) = (^ r (forall x ((thought (left r)) x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) everyone thought he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (forall x ((thought (left r)) x))))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) everyone thought he left ((e > 1) // ((t // (t \\ t)) \\ 1)) = (^ c (^ r (c (^ c (forall x (c ((thought (left r)) x))))))) everyone ((1 // ((t // (2 \\ 3)) \\ 4)) / (1 // ((t // ((e \ 2) \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (forall x (r (^ r (c (r x))))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (1 // (((t // (2 \\ 3)) / (t // ((e \ 2) \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (forall x (R (^ r (c (r x))))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) everyone ((t // (1 \\ 2)) / (t // ((e \ 1) \\ 2))) = (^ R (^ c (forall x (R (^ r (c (r x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) everyone (t // ((1 / (e \ 1)) \\ t)) = (^ c (forall x (c (^ f (f x))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) everyone (t // (e \\ t)) = (^ k (forall x (k x))) thought he left ((e > 1) // ((2 // ((e \ t) \\ 2)) \\ 1)) = (^ c (^ r (c (^ c (c (thought (left r))))))) thought ((1 // ((2 // ((e \ t) \\ 3)) \\ 4)) / (1 // ((2 // (t \\ 3)) \\ 4))) = (^ R (^ c (R (^ r (c (^ c (r (^ r (c (thought r)))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((2 // ((e \ t) \\ 3)) / (2 // (t \\ 3))) \\ 1)) = (^ f (f (^ R (^ c (R (^ r (c (thought r)))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((1 // ((e \ t) \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c (thought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) thought (1 // (((e \ t) / t) \\ 1)) = (^ f (f thought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) thought ((e \ t) / t) = thought he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he left ((e > 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (left r)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) he left ((e > 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left 513 edges -- Done parsing. # (Processing: (he saw him)) ------------------- edge : 140 he saw him (0 3) (e > (e > t)) semantics : (^ r (^ r1 ((saw r1) r))) proofnet : (((1 . e) > ((2 . e) > (3 . t))) (he (((1 . e) > ((2 . e) > (3 . t))) // ((4 . e) \\ ((2 . e) > (3 . t))))) (saw (((4 . e) \ (5 . t)) / (6 . e))) (him (((2 . e) > (3 . t)) // ((6 . e) \\ (3 . t))))) derivation: (D ((S ((S (U L)) he)) ((S (U saw)) him))) he saw him (e > (e > t)) = (^ r (^ r1 ((saw r1) r))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) he saw him ((e > (e > 1)) // (t \\ 1)) = (^ c (^ r (^ r1 (c ((saw r1) r))))) he (((e > 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) he ((e > 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) he ((e > 1) // (e \\ 1)) = (^ k k) saw him ((e > 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (saw r)))) saw ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (saw r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) saw (1 // (((e \ t) / e) \\ 1)) = (^ f (f saw)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) saw ((e \ t) / e) = saw him ((e > 1) // (e \\ 1)) = (^ k k) 251 edges -- Done parsing. # #unspecified (Processing: (who left)) ------------------- edge : 124 who left (0 2) (e ? t) semantics : (^ r (left r)) proofnet : (((1 . e) ? (2 . t)) (who (((1 . e) ? (2 . t)) // ((3 . e) \\ (2 . t)))) (left ((3 . e) \ (4 . t)))) derivation: (D ((S ((S (U L)) who)) (U left))) who left (e ? t) = (^ r (left r)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) who left ((e ? 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) who (((e ? 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) who ((e ? 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) who ((e ? 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left 295 edges -- Done parsing. # (Processing: (who bought what)) ------------------- edge : 222 who bought what (0 3) (e ? (e ? t)) semantics : (^ r (^ r1 ((bought r1) r))) proofnet : (((1 . e) ? ((2 . e) ? (3 . t))) (who (((1 . e) ? ((2 . e) ? (3 . t))) // ((4 . e) \\ ((2 . e) ? (3 . t))))) (bought (((4 . e) \ (5 . t)) / (6 . e))) (what (((2 . e) ? (3 . t)) // ((6 . e) \\ (3 . t))))) derivation: (D ((S ((S (U L)) who)) ((S (U bought)) what))) who bought what (e ? (e ? t)) = (^ r (^ r1 ((bought r1) r))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) who bought what ((e ? (e ? 1)) // (t \\ 1)) = (^ c (^ r (^ r1 (c ((bought r1) r))))) who (((e ? 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) who ((e ? 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) who ((e ? 1) // (e \\ 1)) = (^ k k) bought what ((e ? 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (bought r)))) bought ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (bought r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) bought (1 // (((e \ t) / e) \\ 1)) = (^ f (f bought)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) bought ((e \ t) / e) = bought what ((e ? 1) // (e \\ 1)) = (^ k k) 463 edges -- Done parsing. # (Processing: (whose mother left)) ------------------- edge : 202 whose mother left (0 3) (e ? t) semantics : (^ r (left (mother r))) proofnet : (((1 . e) ? (2 . t)) (whose (((1 . e) ? (2 . t)) // ((3 . e) \\ (2 . t)))) (mother ((3 . e) \ (4 . e))) (left ((4 . e) \ (5 . t)))) derivation: (D ((S ((S (U L)) ((S ((S (U L)) whose)) (U mother)))) (U left))) whose mother left (e ? t) = (^ r (left (mother r))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) whose mother left ((e ? 1) // (t \\ 1)) = (^ c (^ r (c (left (mother r))))) whose mother (((e ? 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 (mother r)))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) whose mother ((e ? 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f (mother r)))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) whose mother ((e ? 1) // (e \\ 1)) = (^ c (^ r (c (mother r)))) whose (((e ? 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) whose ((e ? 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) whose ((e ? 1) // (e \\ 1)) = (^ k k) mother (1 // ((e \ e) \\ 1)) = (^ f (f mother)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mother (e \ e) = mother left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left 390 edges -- Done parsing. # (Processing: (who _ left)) ------------------- edge : 181 who _ left (0 3) (e ? t) semantics : (^ r (left r)) proofnet : (((1 . e) ? (2 . t)) (who (((3 . e) ? (2 . t)) // ((4 . e) \\ (2 . t)))) (_ (((4 . e) \\ (2 . t)) // ((5 . e) \\ (2 . t)))) (left ((5 . e) \ (6 . t)))) derivation: ((Q who) (D ((S ((S (U L)) _)) (U left)))) who _ left (e ? t) = (^ r (left r)) who ((e ? 1) / (e \\ 1)) = (^ k k) Q (((e ? 1) / 2) / ((e ? 1) // 2)) = (^ k k) who ((e ? 1) // (e \\ 1)) = (^ k k) _ left (e \\ t) = (^ r (left r)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) _ left ((e \\ 1) // (t \\ 1)) = (^ c (^ r (c (left r)))) _ (((e \\ 1) // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (^ r (R (^ r1 (c (r1 r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) _ ((e \\ 1) // ((2 / (e \ 2)) \\ 1)) = (^ c (^ r (c (^ f (f r))))) RULE ((1 // ((2 / (3 \ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 / (3 \ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) _ ((e \\ 1) // (e \\ 1)) = (^ k k) left (1 // ((e \ t) \\ 1)) = (^ f (f left)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) left (e \ t) = left 276 edges -- Done parsing. # (Processing: (what did mary buy _)) ------------------- edge : 309 what did mary buy _ (0 5) (e ? t) semantics : (^ r ((buy r) m)) proofnet : (((1 . e) ? (2 . t)) (what (((3 . e) ? (2 . t)) // ((4 . e) \\ (2 . t)))) (did ((5 . t) / (6 . t))) (mary (7 . e)) (buy (((7 . e) \ (6 . t)) / (8 . e))) (_ (((4 . e) \\ (2 . t)) // ((8 . e) \\ (2 . t))))) derivation: ((Q what) (D ((S (U did)) ((S (U (L mary))) ((S (U buy)) _))))) what did mary buy _ (e ? t) = (^ r ((buy r) m)) what ((e ? 1) / (e \\ 1)) = (^ k k) Q (((e ? 1) / 2) / ((e ? 1) // 2)) = (^ k k) what ((e ? 1) // (e \\ 1)) = (^ k k) did mary buy _ (e \\ t) = (^ r ((buy r) m)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) did mary buy _ ((e \\ 1) // (t \\ 1)) = (^ c (^ r (c ((buy r) m)))) did ((1 // (t \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c r))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) did (1 // ((t / t) \\ 1)) = (^ f (f (^ p p))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) did (t / t) = (^ p p) mary buy _ ((e \\ 1) // (t \\ 1)) = (^ c (^ r (c ((buy r) m)))) mary ((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (R (^ r (c (r m)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) mary (1 // ((2 / (e \ 2)) \\ 1)) = (^ f (f (^ f (f m)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mary (1 / (e \ 1)) = (^ f (f m)) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) mary e = m buy _ ((e \\ 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (buy r)))) buy ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (buy r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) buy (1 // (((e \ t) / e) \\ 1)) = (^ f (f buy)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) buy ((e \ t) / e) = buy _ ((e \\ 1) // (e \\ 1)) = (^ k k) ------------------- edge : 401 what did mary buy _ (0 5) (e ? t) semantics : (^ r ((buy r) m)) proofnet : (((1 . e) ? (2 . t)) (what (((3 . e) ? (2 . t)) // ((4 . e) \\ (2 . t)))) (did ((5 . t) / (6 . t))) (mary (7 . e)) (buy (((7 . e) \ (8 . t)) / (9 . e))) (_ (((4 . e) \\ (2 . t)) // ((9 . e) \\ (2 . t))))) derivation: ((Q what) (D ((S (U did)) ((S (U D)) ((S (U U)) ((S (U (L mary))) ((S (U buy)) _))))))) what did mary buy _ (e ? t) = (^ r ((buy r) m)) what ((e ? 1) / (e \\ 1)) = (^ k k) Q (((e ? 1) / 2) / ((e ? 1) // 2)) = (^ k k) what ((e ? 1) // (e \\ 1)) = (^ k k) did mary buy _ (e \\ t) = (^ r ((buy r) m)) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) did mary buy _ ((e \\ 1) // (t \\ 1)) = (^ c (^ r (c ((buy r) m)))) did ((1 // (t \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c r))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) did (1 // ((t / t) \\ 1)) = (^ f (f (^ p p))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) did (t / t) = (^ p p) mary buy _ ((e \\ 1) // (t \\ 1)) = (^ c (^ r (c ((buy r) m)))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) mary buy _ ((e \\ 1) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (c (^ f (f ((buy r) m)))))) RULE ((1 // ((2 // (3 \\ 2)) \\ 4)) / (1 // (3 \\ 4))) = (^ R (^ c (R (^ r (c (^ f (f r))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // (((2 // (3 \\ 2)) / 3) \\ 1)) = (^ f (f (^ x (^ f (f x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mary buy _ ((e \\ 1) // (t \\ 1)) = (^ c (^ r (c ((buy r) m)))) mary ((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (R (^ r (c (r m)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) mary (1 // ((2 / (e \ 2)) \\ 1)) = (^ f (f (^ f (f m)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mary (1 / (e \ 1)) = (^ f (f m)) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) mary e = m buy _ ((e \\ 1) // ((e \ t) \\ 1)) = (^ c (^ r (c (buy r)))) buy ((1 // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (buy r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) buy (1 // (((e \ t) / e) \\ 1)) = (^ f (f buy)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) buy ((e \ t) / e) = buy _ ((e \\ 1) // (e \\ 1)) = (^ k k) 564 edges -- Done parsing. # (Processing: (who did mary give _ what)) ------------------- edge : 399 who did mary give _ what (0 6) (e ? (e ? t)) semantics : (^ r (^ r1 (((give r) r1) m))) proofnet : (((1 . e) ? ((2 . e) ? (3 . t))) (who (((4 . e) ? ((2 . e) ? (3 . t))) // ((5 . e) \\ ((2 . e) ? (3 . t))))) (did ((6 . t) / (7 . t))) (mary (8 . e)) (give ((((8 . e) \ (7 . t)) / (9 . e)) / (10 . e))) (_ (((5 . e) \\ ((2 . e) ? (3 . t))) // ((10 . e) \\ ((2 . e) ? (3 . t))))) (what (((2 . e) ? (3 . t)) // ((9 . e) \\ (3 . t))))) derivation: ((Q who) (D ((S (U did)) ((S (U (L mary))) ((S ((S (U give)) _)) what))))) who did mary give _ what (e ? (e ? t)) = (^ r (^ r1 (((give r) r1) m))) who ((e ? 1) / (e \\ 1)) = (^ k k) Q (((e ? 1) / 2) / ((e ? 1) // 2)) = (^ k k) who ((e ? 1) // (e \\ 1)) = (^ k k) did mary give _ what (e \\ (e ? t)) = (^ r (^ r1 (((give r) r1) m))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) did mary give _ what ((e \\ (e ? 1)) // (t \\ 1)) = (^ c (^ r (^ r1 (c (((give r) r1) m))))) did ((1 // (t \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c r))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) did (1 // ((t / t) \\ 1)) = (^ f (f (^ p p))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) did (t / t) = (^ p p) mary give _ what ((e \\ (e ? 1)) // (t \\ 1)) = (^ c (^ r (^ r1 (c (((give r) r1) m))))) mary ((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (R (^ r (c (r m)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) mary (1 // ((2 / (e \ 2)) \\ 1)) = (^ f (f (^ f (f m)))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mary (1 / (e \ 1)) = (^ f (f m)) L ((2 / (1 \ 2)) / 1) = (^ x (^ f (f x))) mary e = m give _ what ((e \\ (e ? 1)) // ((e \ t) \\ 1)) = (^ c (^ r (^ r1 (c ((give r) r1))))) give _ (((e \\ 1) // ((e \ t) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (^ r (R (^ r1 (c ((give r) r1))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) give _ ((e \\ 1) // (((e \ t) / e) \\ 1)) = (^ c (^ r (c (give r)))) give ((1 // (((e \ t) / e) \\ 2)) / (1 // (e \\ 2))) = (^ R (^ c (R (^ r (c (give r)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) give (1 // ((((e \ t) / e) / e) \\ 1)) = (^ f (f give)) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) give (((e \ t) / e) / e) = give _ ((e \\ 1) // (e \\ 1)) = (^ k k) what ((e ? 1) // (e \\ 1)) = (^ k k) ------------------- edge : 554 who did mary give _ what (0 6) (e ? (e ? t)) semantics : (^ r (^ r1 (((give r) r1) m))) proofnet : (((1 . e) ? ((2 . e) ? (3 . t))) (who (((4 . e) ? ((2 . e) ? (3 . t))) // ((5 . e) \\ ((2 . e) ? (3 . t))))) (did ((6 . t) / (7 . t))) (mary (8 . e)) (give ((((8 . e) \ (9 . t)) / (10 . e)) / (11 . e))) (_ (((5 . e) \\ ((2 . e) ? (3 . t))) // ((11 . e) \\ ((2 . e) ? (3 . t))))) (what (((2 . e) ? (3 . t)) // ((10 . e) \\ (3 . t))))) derivation: ((Q who) (D ((S (U did)) ((S (U D)) ((S (U (S (U (L mary))))) ((S (U U)) ((S ((S (U give)) _)) what))))))) who did mary give _ what (e ? (e ? t)) = (^ r (^ r1 (((give r) r1) m))) who ((e ? 1) / (e \\ 1)) = (^ k k) Q (((e ? 1) / 2) / ((e ? 1) // 2)) = (^ k k) who ((e ? 1) // (e \\ 1)) = (^ k k) did mary give _ what (e \\ (e ? t)) = (^ r (^ r1 (((give r) r1) m))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) did mary give _ what ((e \\ (e ? 1)) // (t \\ 1)) = (^ c (^ r (^ r1 (c (((give r) r1) m))))) did ((1 // (t \\ 2)) / (1 // (t \\ 2))) = (^ R (^ c (R (^ r (c r))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) did (1 // ((t / t) \\ 1)) = (^ f (f (^ p p))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) did (t / t) = (^ p p) mary give _ what ((e \\ (e ? 1)) // (t \\ 1)) = (^ c (^ r (^ r1 (c (((give r) r1) m))))) RULE ((1 // (2 \\ 3)) / (1 // ((2 // (t \\ t)) \\ 3))) = (^ R (^ c (R (^ r (c (r (^ x x))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) RULE (1 // ((2 / (2 // (t \\ t))) \\ 1)) = (^ f (f (^ k (k (^ x x))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) D (1 / (1 // (t \\ t))) = (^ k (k (^ x x))) mary give _ what ((e \\ (e ? 1)) // ((2 // (t \\ 2)) \\ 1)) = (^ c (^ r (^ r1 (c (^ c (c (((give r) r1) m))))))) mary ((1 // ((2 // (3 \\ 4)) \\ 5)) / (1 // ((2 // ((e \ 3) \\ 4)) \\ 5))) = (^ R (^ c (R (^ r (c (^ c (r (^ r (c (r m)))))))))) S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))) = (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))) mary (1 // (((2 // (3 \\ 4)) / (2 // ((e \ 3) \\ 4))) \\ 1)) = (^ f (f (^ R (^ c (R (^ r (c (r m)))))))) U ((2 // (1 \\ 2)) / 1) = (^ x (^ f (f x))) mary ((1 // (2 \\ 3)) / (1 // ((e \ 2) \\ 3))) = (^ R (^ c (R (^ r (c (r m)))))) S (((4 // (2 \\ 5)) / (3 // (1 \\