The cow eats the dog. The dog eats the cow. The mouse visits the dog. The rabbit needs the cow. If someone needs the mouse and they need the cow then they visit the dog. If someone visits the dog and they are red then the dog eats the mouse. If someone visits the rabbit then they are nice. If the dog needs the mouse and the dog is round then the mouse needs the rabbit. If someone visits the mouse then the mouse is rough. If the dog is young and the dog visits the rabbit then the rabbit is nice. If someone visits the dog then the dog visits the mouse. If someone is rough then they need the cow.
The cow eats the dog.
("cow" "eats" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If someone needs the mouse and they need the cow then they visit the dog.
((("someone" "needs" "mouse" "+") ("someone" "needs" "cow" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the dog and they are red then the dog eats the mouse.
((("someone" "visits" "dog" "+") ("someone" "is" "red" "+")) -> ("dog" "eats" "mouse" "+"))
If someone visits the rabbit then they are nice.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "nice" "+"))
If the dog needs the mouse and the dog is round then the mouse needs the rabbit.
((("dog" "needs" "mouse" "+") ("dog" "is" "round" "+")) -> ("mouse" "needs" "rabbit" "+"))
If someone visits the mouse then the mouse is rough.
((("someone" "visits" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If the dog is young and the dog visits the rabbit then the rabbit is nice.
((("dog" "is" "young" "+") ("dog" "visits" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If someone visits the dog then the dog visits the mouse.
((("someone" "visits" "dog" "+")) -> ("dog" "visits" "mouse" "+"))
If someone is rough then they need the cow.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "cow" "+"))
The dog eats the cow.
True
1
proof
[(triple2)]
("dog" "eats" "cow" "+")
triple2
The cow does not eat the dog.
False
1
inv-proof
[(triple1)]
("cow" "eats" "dog" "-")
triple1
The dog visits the mouse.
True
2
proof
[(((triple3) -> rule7))]
("dog" "visits" "mouse" "+")
((triple3) -> (rule7 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog does not visit the mouse.
False
2
inv-proof
[(((triple3) -> rule7))]
("dog" "visits" "mouse" "-")
((triple3) -> (rule7 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple3) -> rule7)) -> rule5))]
("mouse" "is" "rough" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The mouse is not rough.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule5))]
("mouse" "is" "rough" "-")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The mouse needs the cow.
True
4
proof
[(((((((triple3) -> rule7)) -> rule5)) -> rule8))]
("mouse" "needs" "cow" "+")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The mouse does not need the cow.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule5)) -> rule8))]
("mouse" "needs" "cow" "-")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The cow does not visit the dog.
Unknown
inv-rconc
[@1: The cow visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "dog" "-")
The dog needs the cow.
Unknown
rconc
[@1: The dog needs the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "needs" "cow" "+")
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "nice" "-")
The dog eats the mouse.
Unknown
rconc
[@1: The dog eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "mouse" "+")
The mouse does not eat the cow.
Unknown
inv-random
[@0: The mouse eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cow" "-")
The rabbit eats the cow.
Unknown
random
[@0: The rabbit eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cow" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The cow eats the dog.[(triple1)] The dog eats the cow.[(triple2)] The mouse visits the dog.[(triple3)] The rabbit needs the cow.[(triple4)] @1: The dog visits the mouse.[(((triple3) -> rule7))] @2: The mouse is rough.[(((((triple3) -> rule7)) -> rule5))] @3: The mouse needs the cow.[(((((((triple3) -> rule7)) -> rule5)) -> rule8))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The dog eats the cow.
("dog" "eats" "cow" "+")
triple2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple4
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((triple3) -> (rule7 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3