The dog is big. The mouse likes the dog. The rabbit does not visit the squirrel. The squirrel visits the mouse. If the dog likes the mouse then the mouse likes the dog. If someone likes the dog and they are not blue then they like the rabbit. If someone likes the rabbit then they are green. If someone likes the dog then the dog likes the rabbit. If someone is green then they visit the mouse. If the squirrel visits the dog and the dog is not blue then the squirrel likes the rabbit. If someone eats the dog and the dog eats the squirrel then the dog likes the squirrel. If someone is green and they like the dog then the dog eats the squirrel.
The dog is big.
("dog" "is" "big" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The rabbit does not visit the squirrel.
("rabbit" "visits" "squirrel" "-")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If the dog likes the mouse then the mouse likes the dog.
((("dog" "likes" "mouse" "+")) -> ("mouse" "likes" "dog" "+"))
If someone likes the dog and they are not blue then they like the rabbit.
((("someone" "likes" "dog" "+") ("someone" "is" "blue" "~")) -> ("someone" "likes" "rabbit" "+"))
If someone likes the rabbit then they are green.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "green" "+"))
If someone likes the dog then the dog likes the rabbit.
((("someone" "likes" "dog" "+")) -> ("dog" "likes" "rabbit" "+"))
If someone is green then they visit the mouse.
((("someone" "is" "green" "+")) -> ("someone" "visits" "mouse" "+"))
If the squirrel visits the dog and the dog is not blue then the squirrel likes the rabbit.
((("squirrel" "visits" "dog" "+") ("dog" "is" "blue" "~")) -> ("squirrel" "likes" "rabbit" "+"))
If someone eats the dog and the dog eats the squirrel then the dog likes the squirrel.
((("someone" "eats" "dog" "+") ("dog" "eats" "squirrel" "+")) -> ("dog" "likes" "squirrel" "+"))
If someone is green and they like the dog then the dog eats the squirrel.
((("someone" "is" "green" "+") ("someone" "likes" "dog" "+")) -> ("dog" "eats" "squirrel" "+"))
The mouse likes the dog.
True
1
proof
[(triple2)]
("mouse" "likes" "dog" "+")
triple2
The dog is not big.
False
1
inv-proof
[(triple1)]
("dog" "is" "big" "-")
triple1
The dog likes the rabbit.
True
2
proof
[(((triple2) -> rule4))]
("dog" "likes" "rabbit" "+")
((triple2) -> (rule4 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog does not like the rabbit.
False
2
inv-proof
[(((triple2) -> rule4))]
("dog" "likes" "rabbit" "-")
((triple2) -> (rule4 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog is green.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("dog" "is" "green" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The dog is not green.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("dog" "is" "green" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The dog visits the mouse.
True
4
proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule5))]
("dog" "visits" "mouse" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3
The dog does not visit the mouse.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule5))]
("dog" "visits" "mouse" "-")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3
The dog does not eat the squirrel.
Unknown
inv-rconc
[@3: The dog eats the squirrel.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule2 <- FAIL)]]
("dog" "eats" "squirrel" "-")
The dog likes the squirrel.
Unknown
rconc
[@1: The dog likes the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "likes" "squirrel" "+")
The rabbit is not green.
Unknown
inv-rconc
[@2: The rabbit is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("rabbit" "is" "green" "-")
The mouse visits the mouse.
Unknown
rconc
[@3: The mouse visits the mouse.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule2 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The dog does not visit the rabbit.
Unknown
inv-random
[@0: The dog visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "rabbit" "-")
The squirrel likes the mouse.
Unknown
random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "+")
@0: The dog is big.[(triple1)] The mouse likes the dog.[(triple2)] The rabbit does not visit the squirrel.[(triple3)] The squirrel visits the mouse.[(triple4)] @1: The dog likes the rabbit.[(((triple2) -> rule4))] @2: The dog is green.[(((((triple2) -> rule4)) -> rule3))] @3: The dog visits the mouse.[(((((((triple2) -> rule4)) -> rule3)) -> rule5))]
The dog is big.
("dog" "is" "big" "+")
triple1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple2
The rabbit does not visit the squirrel.
("rabbit" "visits" "squirrel" "-")
triple3
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple4
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
((triple2) -> (rule4 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog is green.
("dog" "is" "green" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3