The cow is nice. The cow is rough. The cow likes the dog. The cow needs the dog. The cow needs the mouse. The dog is cold. The mouse is nice. If someone chases the dog then the dog is rough. If someone chases the mouse and they chase the dog then the mouse likes the dog. If someone is blue then they need the mouse. If someone needs the dog then they are nice. If someone likes the dog and they need the mouse then they like the mouse. If someone is rough and they like the mouse then the mouse likes the cow. If someone needs the mouse then the mouse chases the dog. If someone needs the mouse and the mouse needs the cow then they chase the cow.
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The dog is cold.
("dog" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
If someone chases the dog then the dog is rough.
((("someone" "chases" "dog" "+")) -> ("dog" "is" "rough" "+"))
If someone chases the mouse and they chase the dog then the mouse likes the dog.
((("someone" "chases" "mouse" "+") ("someone" "chases" "dog" "+")) -> ("mouse" "likes" "dog" "+"))
If someone is blue then they need the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the dog then they are nice.
((("someone" "needs" "dog" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the dog and they need the mouse then they like the mouse.
((("someone" "likes" "dog" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is rough and they like the mouse then the mouse likes the cow.
((("someone" "is" "rough" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "cow" "+"))
If someone needs the mouse then the mouse chases the dog.
((("someone" "needs" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If someone needs the mouse and the mouse needs the cow then they chase the cow.
((("someone" "needs" "mouse" "+") ("mouse" "needs" "cow" "+")) -> ("someone" "chases" "cow" "+"))
The cow needs the dog.
True
1
proof
[(triple4)]
("cow" "needs" "dog" "+")
triple4
The cow does not like the dog.
False
1
inv-proof
[(triple3)]
("cow" "likes" "dog" "-")
triple3
The mouse chases the dog.
True
2
proof
[(((triple5) -> rule7))]
("mouse" "chases" "dog" "+")
((triple5) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The cow does not like the mouse.
False
3
inv-proof
[(((triple3 triple5) -> rule5))]
("cow" "likes" "mouse" "-")
((triple3 triple5) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The dog is rough.
True
3
proof
[(((((triple5) -> rule7)) -> rule1))]
("dog" "is" "rough" "+")
((((triple5) -> (rule7 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The mouse does not like the cow.
False
5
inv-proof
[(((triple2 ((triple3 triple5) -> rule5)) -> rule6))]
("mouse" "likes" "cow" "-")
((triple2 ((triple3 triple5) -> (rule5 % int2))) -> (rule6 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The dog does not like the mouse.
Unknown
inv-rconc
[@1: The dog likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "likes" "mouse" "-")
The dog chases the cow.
Unknown
rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "chases" "cow" "+")
The mouse does not chase the cow.
Unknown
inv-rconc
[@1: The mouse chases the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "chases" "cow" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow is nice.[(triple1 OR ((triple4) -> rule4))] The cow is rough.[(triple2)] The cow likes the dog.[(triple3)] The cow needs the dog.[(triple4)] The cow needs the mouse.[(triple5)] The dog is cold.[(triple6)] The mouse is nice.[(triple7)] @1: The cow likes the mouse.[(((triple3 triple5) -> rule5))] The mouse chases the dog.[(((triple5) -> rule7))] @2: The dog is rough.[(((((triple5) -> rule7)) -> rule1))] The mouse likes the cow.[(((triple2 ((triple3 triple5) -> rule5)) -> rule6))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
((triple4) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow likes the dog.
("cow" "likes" "dog" "+")
triple3
The cow needs the dog.
("cow" "needs" "dog" "+")
triple4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple5
The dog is cold.
("dog" "is" "cold" "+")
triple6
The mouse is nice.
("mouse" "is" "nice" "+")
triple7
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((triple3 triple5) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((triple5) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((((triple5) -> (rule7 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((triple2 ((triple3 triple5) -> (rule5 % int2))) -> (rule6 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2