The dog is rough. The mouse is red. The mouse likes the dog. If the mouse sees the dog and the dog likes the mouse then the mouse is red. If the dog likes the mouse and the mouse likes the dog then the mouse is red. If something eats the mouse then it sees the mouse. If something likes the mouse and it sees the mouse then it eats the mouse. If something is rough and it sees the dog then it is big. If something eats the mouse then it is kind. If something sees the mouse then it sees the dog. If something is red and it likes the dog then the dog sees the mouse.
The dog is rough.
("dog" "is" "rough" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
If the mouse sees the dog and the dog likes the mouse then the mouse is red.
((("mouse" "sees" "dog" "+") ("dog" "likes" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If the dog likes the mouse and the mouse likes the dog then the mouse is red.
((("dog" "likes" "mouse" "+") ("mouse" "likes" "dog" "+")) -> ("mouse" "is" "red" "+"))
If something eats the mouse then it sees the mouse.
((("something" "eats" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
If something likes the mouse and it sees the mouse then it eats the mouse.
((("something" "likes" "mouse" "+") ("something" "sees" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
If something is rough and it sees the dog then it is big.
((("something" "is" "rough" "+") ("something" "sees" "dog" "+")) -> ("something" "is" "big" "+"))
If something eats the mouse then it is kind.
((("something" "eats" "mouse" "+")) -> ("something" "is" "kind" "+"))
If something sees the mouse then it sees the dog.
((("something" "sees" "mouse" "+")) -> ("something" "sees" "dog" "+"))
If something is red and it likes the dog then the dog sees the mouse.
((("something" "is" "red" "+") ("something" "likes" "dog" "+")) -> ("dog" "sees" "mouse" "+"))
The mouse likes the dog.
True
1
proof
[(triple3)]
("mouse" "likes" "dog" "+")
triple3
The mouse is not red.
False
1
inv-proof
[(triple2)]
("mouse" "is" "red" "-")
triple2
The dog sees the mouse.
True
3
proof
[(((triple2 triple3) -> rule8))]
("dog" "sees" "mouse" "+")
((triple2 triple3) -> (rule8 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog does not see the mouse.
False
3
inv-proof
[(((triple2 triple3) -> rule8))]
("dog" "sees" "mouse" "-")
((triple2 triple3) -> (rule8 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog sees the dog.
True
4
proof
[(((((triple2 triple3) -> rule8)) -> rule7))]
("dog" "sees" "dog" "+")
((((triple2 triple3) -> (rule8 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog does not see the dog.
False
4
inv-proof
[(((((triple2 triple3) -> rule8)) -> rule7))]
("dog" "sees" "dog" "-")
((((triple2 triple3) -> (rule8 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog is big.
True
6
proof
[(((triple1 ((((triple2 triple3) -> rule8)) -> rule7)) -> rule5))]
("dog" "is" "big" "+")
((triple1 ((((triple2 triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The dog is not big.
False
6
inv-proof
[(((triple1 ((((triple2 triple3) -> rule8)) -> rule7)) -> rule5))]
("dog" "is" "big" "-")
((triple1 ((((triple2 triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The dog eats the mouse.
Unknown
rconc
[@1: The dog eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "eats" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-rconc
[@2: The mouse sees the mouse.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is kind.
Unknown
rconc
[@2: The mouse is kind.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("mouse" "is" "kind" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The dog is rough.[(triple1)] The mouse is red.[(triple2)] The mouse likes the dog.[(triple3)] @1: The dog sees the mouse.[(((triple2 triple3) -> rule8))] @2: The dog sees the dog.[(((((triple2 triple3) -> rule8)) -> rule7))] @3: The dog is big.[(((triple1 ((((triple2 triple3) -> rule8)) -> rule7)) -> rule5))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((triple2 triple3) -> (rule8 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple2 triple3) -> (rule8 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog is big.
("dog" "is" "big" "+")
((triple1 ((((triple2 triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3