The cow eats the tiger. The cow likes the tiger. The cow sees the dog. The cow sees the tiger. The dog eats the mouse. The dog is red. The dog sees the mouse. The mouse eats the dog. The mouse is big. The mouse is rough. The mouse likes the cow. The mouse likes the dog. The tiger eats the mouse. The tiger sees the dog. The tiger sees the mouse. If something likes the mouse and it likes the cow then the cow is red. If something likes the dog then it likes the mouse.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is red.
("dog" "is" "red" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something likes the mouse and it likes the cow then the cow is red.
((("something" "likes" "mouse" "+") ("something" "likes" "cow" "+")) -> ("cow" "is" "red" "+"))
If something likes the dog then it likes the mouse.
((("something" "likes" "dog" "+")) -> ("something" "likes" "mouse" "+"))
The cow sees the tiger.
True
1
proof
[(triple4)]
("cow" "sees" "tiger" "+")
triple4
The dog does not eat the mouse.
False
1
inv-proof
[(triple5)]
("dog" "eats" "mouse" "-")
triple5
The mouse likes the mouse.
True
2
proof
[(((triple12) -> rule2))]
("mouse" "likes" "mouse" "+")
((triple12) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple12) -> rule2))]
("mouse" "likes" "mouse" "-")
((triple12) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cow is red.
True
4
proof
[(((((triple12) -> rule2) triple11) -> rule1))]
("cow" "is" "red" "+")
((((triple12) -> (rule2 % int2)) triple11) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The cow is not red.
False
4
inv-proof
[(((((triple12) -> rule2) triple11) -> rule1))]
("cow" "is" "red" "-")
((((triple12) -> (rule2 % int2)) triple11) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The cow does not like the mouse.
Unknown
inv-rconc
[@1: The cow likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "mouse" "-")
The tiger likes the mouse.
Unknown
rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "mouse" "+")
The dog does not like the mouse.
Unknown
inv-rconc
[@1: The dog likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "likes" "mouse" "-")
The dog sees the tiger.
Unknown
random
[@0: The dog sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "tiger" "+")
The tiger does not see the cow.
Unknown
inv-random
[@0: The tiger sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cow" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cow eats the tiger.[(triple1)] The cow likes the tiger.[(triple2)] The cow sees the dog.[(triple3)] The cow sees the tiger.[(triple4)] The dog eats the mouse.[(triple5)] The dog is red.[(triple6)] The dog sees the mouse.[(triple7)] The mouse eats the dog.[(triple8)] The mouse is big.[(triple9)] The mouse is rough.[(triple10)] The mouse likes the cow.[(triple11)] The mouse likes the dog.[(triple12)] The tiger eats the mouse.[(triple13)] The tiger sees the dog.[(triple14)] The tiger sees the mouse.[(triple15)] @1: The mouse likes the mouse.[(((triple12) -> rule2))] @2: The cow is red.[(((((triple12) -> rule2) triple11) -> rule1))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple4
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple7
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse is rough.
("mouse" "is" "rough" "+")
triple10
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple11
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple12
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple13
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple12) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((((triple12) -> (rule2 % int2)) triple11) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2