The dog chases the mouse. The dog is kind. The dog is nice. The dog is red. The dog is rough. The dog likes the mouse. The dog visits the mouse. The mouse chases the dog. The mouse is big. The mouse is nice. The mouse is red. The mouse likes the dog. If someone chases the dog and the dog chases the mouse then they visit the dog. If the mouse is kind then the mouse is big. If someone likes the mouse and they visit the dog then the mouse chases the dog. If someone is big and they like the mouse then they chase the dog. If the dog chases the mouse and the dog is red then the dog is big. If the dog likes the mouse then the dog is big.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
If someone chases the dog and the dog chases the mouse then they visit the dog.
((("someone" "chases" "dog" "+") ("dog" "chases" "mouse" "+")) -> ("someone" "visits" "dog" "+"))
If the mouse is kind then the mouse is big.
((("mouse" "is" "kind" "+")) -> ("mouse" "is" "big" "+"))
If someone likes the mouse and they visit the dog then the mouse chases the dog.
((("someone" "likes" "mouse" "+") ("someone" "visits" "dog" "+")) -> ("mouse" "chases" "dog" "+"))
If someone is big and they like the mouse then they chase the dog.
((("someone" "is" "big" "+") ("someone" "likes" "mouse" "+")) -> ("someone" "chases" "dog" "+"))
If the dog chases the mouse and the dog is red then the dog is big.
((("dog" "chases" "mouse" "+") ("dog" "is" "red" "+")) -> ("dog" "is" "big" "+"))
If the dog likes the mouse then the dog is big.
((("dog" "likes" "mouse" "+")) -> ("dog" "is" "big" "+"))
The dog is rough.
True
1
proof
[(triple5)]
("dog" "is" "rough" "+")
triple5
The dog does not visit the mouse.
False
1
inv-proof
[(triple7)]
("dog" "visits" "mouse" "-")
triple7
The mouse visits the dog.
True
3
proof
[(((triple8 triple1) -> rule1) OR ((((triple6 ((((((triple6) -> rule6) triple6) -> rule4) triple1) -> rule1)) -> rule3) triple1) -> rule1) OR ((((triple6 ((((((triple1 triple4) -> rule5) triple6) -> rule4) triple1) -> rule1)) -> rule3) triple1) -> rule1))]
("mouse" "visits" "dog" "+")
((triple8 triple1) -> (rule1 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
((((triple6 ((((((triple6) -> (rule6 % int5)) triple6) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog chases the dog.
("dog" "chases" "dog" "+")
int4
The dog is big.
("dog" "is" "big" "+")
int5
((((triple6 ((((((triple1 triple4) -> (rule5 % int5)) triple6) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog chases the dog.
("dog" "chases" "dog" "+")
int4
The dog is big.
("dog" "is" "big" "+")
int5
The dog is not big.
False
2
inv-proof
[(((triple6) -> rule6) OR ((triple1 triple4) -> rule5))]
("dog" "is" "big" "-")
((triple6) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
((triple1 triple4) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog chases the dog.
True
4
proof
[(((((triple6) -> rule6) triple6) -> rule4) OR ((((triple1 triple4) -> rule5) triple6) -> rule4))]
("dog" "chases" "dog" "+")
((((triple6) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
((((triple1 triple4) -> (rule5 % int2)) triple6) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog does not chase the dog.
False
4
inv-proof
[(((((triple6) -> rule6) triple6) -> rule4) OR ((((triple1 triple4) -> rule5) triple6) -> rule4))]
("dog" "chases" "dog" "-")
((((triple6) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
((((triple1 triple4) -> (rule5 % int2)) triple6) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog visits the dog.
True
6
proof
[(((((((triple6) -> rule6) triple6) -> rule4) triple1) -> rule1) OR ((((((triple1 triple4) -> rule5) triple6) -> rule4) triple1) -> rule1))]
("dog" "visits" "dog" "+")
((((((triple6) -> (rule6 % int3)) triple6) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
((((((triple1 triple4) -> (rule5 % int3)) triple6) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog does not visit the dog.
False
6
inv-proof
[(((((((triple6) -> rule6) triple6) -> rule4) triple1) -> rule1) OR ((((((triple1 triple4) -> rule5) triple6) -> rule4) triple1) -> rule1))]
("dog" "visits" "dog" "-")
((((((triple6) -> (rule6 % int3)) triple6) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
((((((triple1 triple4) -> (rule5 % int3)) triple6) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The dog chases the mouse.[(triple1)] The dog is kind.[(triple2)] The dog is nice.[(triple3)] The dog is red.[(triple4)] The dog is rough.[(triple5)] The dog likes the mouse.[(triple6)] The dog visits the mouse.[(triple7)] The mouse chases the dog.[(triple8 OR ((triple6 ((((((triple6) -> rule6) triple6) -> rule4) triple1) -> rule1)) -> rule3) OR ((triple6 ((((((triple1 triple4) -> rule5) triple6) -> rule4) triple1) -> rule1)) -> rule3))] The mouse is big.[(triple9)] The mouse is nice.[(triple10)] The mouse is red.[(triple11)] The mouse likes the dog.[(triple12)] @1: The dog is big.[(((triple6) -> rule6) OR ((triple1 triple4) -> rule5))] The mouse visits the dog.[(((triple8 triple1) -> rule1) OR ((((triple6 ((((((triple6) -> rule6) triple6) -> rule4) triple1) -> rule1)) -> rule3) triple1) -> rule1) OR ((((triple6 ((((((triple1 triple4) -> rule5) triple6) -> rule4) triple1) -> rule1)) -> rule3) triple1) -> rule1))] @2: The dog chases the dog.[(((((triple6) -> rule6) triple6) -> rule4) OR ((((triple1 triple4) -> rule5) triple6) -> rule4))] @3: The dog visits the dog.[(((((((triple6) -> rule6) triple6) -> rule4) triple1) -> rule1) OR ((((((triple1 triple4) -> rule5) triple6) -> rule4) triple1) -> rule1))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple6
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple7
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple8
((triple6 ((((((triple6) -> (rule6 % int4)) triple6) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
int3
The dog is big.
("dog" "is" "big" "+")
int4
((triple6 ((((((triple1 triple4) -> (rule5 % int4)) triple6) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
int3
The dog is big.
("dog" "is" "big" "+")
int4
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse is nice.
("mouse" "is" "nice" "+")
triple10
The mouse is red.
("mouse" "is" "red" "+")
triple11
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple12
The dog is big.
("dog" "is" "big" "+")
((triple6) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
((triple1 triple4) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((triple8 triple1) -> (rule1 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
((((triple6 ((((((triple6) -> (rule6 % int5)) triple6) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog chases the dog.
("dog" "chases" "dog" "+")
int4
The dog is big.
("dog" "is" "big" "+")
int5
((((triple6 ((((((triple1 triple4) -> (rule5 % int5)) triple6) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog chases the dog.
("dog" "chases" "dog" "+")
int4
The dog is big.
("dog" "is" "big" "+")
int5
The dog chases the dog.
("dog" "chases" "dog" "+")
((((triple6) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
((((triple1 triple4) -> (rule5 % int2)) triple6) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((triple6) -> (rule6 % int3)) triple6) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
((((((triple1 triple4) -> (rule5 % int3)) triple6) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3