The dog chases the mouse. The dog eats the mouse. The dog is blue. The dog is cold. The dog is kind. The dog is rough. The dog is young. The dog sees the mouse. The mouse chases the dog. The mouse eats the dog. The mouse is blue. The mouse is cold. The mouse is kind. The mouse is young. The mouse sees the dog. If someone is blue and they see the dog then the dog chases the mouse. If someone is young then they eat the dog. If someone is blue and they eat the mouse then the mouse is cold. If the mouse chases the dog then the dog eats the mouse. If someone eats the mouse then the mouse sees the dog. If someone is rough and they see the dog then the dog is kind.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If someone is blue and they see the dog then the dog chases the mouse.
((("someone" "is" "blue" "+") ("someone" "sees" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
If someone is young then they eat the dog.
((("someone" "is" "young" "+")) -> ("someone" "eats" "dog" "+"))
If someone is blue and they eat the mouse then the mouse is cold.
((("someone" "is" "blue" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If the mouse chases the dog then the dog eats the mouse.
((("mouse" "chases" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
If someone eats the mouse then the mouse sees the dog.
((("someone" "eats" "mouse" "+")) -> ("mouse" "sees" "dog" "+"))
If someone is rough and they see the dog then the dog is kind.
((("someone" "is" "rough" "+") ("someone" "sees" "dog" "+")) -> ("dog" "is" "kind" "+"))
The dog eats the mouse.
True
1
proof
[(triple2 OR ((triple9) -> rule4))]
("dog" "eats" "mouse" "+")
triple2
((triple9) -> (rule4 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse is not kind.
False
1
inv-proof
[(triple13)]
("mouse" "is" "kind" "-")
triple13
The dog eats the dog.
True
2
proof
[(((triple7) -> rule2))]
("dog" "eats" "dog" "+")
((triple7) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog does not eat the dog.
False
2
inv-proof
[(((triple7) -> rule2))]
("dog" "eats" "dog" "-")
((triple7) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The dog chases the mouse.[(triple1 OR ((triple11 triple15) -> rule1) OR ((triple11 ((triple2) -> rule5)) -> rule1) OR ((triple11 ((((triple9) -> rule4)) -> rule5)) -> rule1))] The dog eats the mouse.[(triple2 OR ((triple9) -> rule4))] The dog is blue.[(triple3)] The dog is cold.[(triple4)] The dog is kind.[(triple5)] The dog is rough.[(triple6)] The dog is young.[(triple7)] The dog sees the mouse.[(triple8)] The mouse chases the dog.[(triple9)] The mouse eats the dog.[(triple10 OR ((triple14) -> rule2))] The mouse is blue.[(triple11)] The mouse is cold.[(triple12 OR ((triple3 triple2) -> rule3) OR ((triple3 ((triple9) -> rule4)) -> rule3))] The mouse is kind.[(triple13)] The mouse is young.[(triple14)] The mouse sees the dog.[(triple15 OR ((triple2) -> rule5) OR ((((triple9) -> rule4)) -> rule5))] @1: The dog eats the dog.[(((triple7) -> rule2))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
((triple11 triple15) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
((triple11 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
((triple11 ((((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple2
((triple9) -> (rule4 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is cold.
("dog" "is" "cold" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple8
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple9
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple10
((triple14) -> (rule2 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
triple11
The mouse is cold.
("mouse" "is" "cold" "+")
triple12
((triple3 triple2) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((triple3 ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
triple13
The mouse is young.
("mouse" "is" "young" "+")
triple14
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple15
((triple2) -> (rule5 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple7) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1