The cow sees the mouse. The mouse chases the cow. The mouse does not chase the tiger. The mouse is cold. The mouse is red. The mouse likes the tiger. The mouse does not see the cow. The mouse sees the tiger. The tiger is red. The tiger is rough. The tiger is young. The tiger likes the cow. If something chases the mouse and it is young then it chases the tiger. If something is rough then it does not like the tiger. If something chases the cow then it does not see the mouse. Blue things are red. If something sees the mouse then it is not blue. If something is blue then it is cold. If something is rough and it does not like the tiger then it does not like the mouse. If something chases the tiger and it is not young then it does not like the mouse.
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If something chases the mouse and it is young then it chases the tiger.
((("something" "chases" "mouse" "+") ("something" "is" "young" "+")) -> ("something" "chases" "tiger" "+"))
If something is rough then it does not like the tiger.
((("something" "is" "rough" "+")) -> ("something" "likes" "tiger" "-"))
If something chases the cow then it does not see the mouse.
((("something" "chases" "cow" "+")) -> ("something" "sees" "mouse" "-"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something sees the mouse then it is not blue.
((("something" "sees" "mouse" "+")) -> ("something" "is" "blue" "-"))
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is rough and it does not like the tiger then it does not like the mouse.
((("something" "is" "rough" "+") ("something" "likes" "tiger" "~")) -> ("something" "likes" "mouse" "-"))
If something chases the tiger and it is not young then it does not like the mouse.
((("something" "chases" "tiger" "+") ("something" "is" "young" "~")) -> ("something" "likes" "mouse" "-"))
The mouse sees the tiger.
True
1
proof
[(triple8)]
("mouse" "sees" "tiger" "+")
triple8
The cow does not see the mouse.
False
1
inv-proof
[(triple1)]
("cow" "sees" "mouse" "-")
triple1
The mouse does not see the mouse.
True
2
proof
[(((triple2) -> rule3))]
("mouse" "sees" "mouse" "-")
((triple2) -> (rule3 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The mouse sees the mouse.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "sees" "mouse" "+")
((triple2) -> (rule3 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The tiger does not like the mouse.
True
4
proof
[(((triple10 ((triple10) -> rule2)) -> rule7))]
("tiger" "likes" "mouse" "-")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule7 % int1))
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
int1
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int2
The tiger likes the mouse.
False
4
inv-proof
[(((triple10 ((triple10) -> rule2)) -> rule7))]
("tiger" "likes" "mouse" "+")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule7 % int1))
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
int1
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int2
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "red" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "cold" "+")
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger sees the cow.
Unknown
random
[@0: The tiger sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cow" "+")
@0: The cow sees the mouse.[(triple1)] The mouse chases the cow.[(triple2)] The mouse does not chase the tiger.[(triple3)] The mouse does not see the cow.[(triple7)] The mouse is cold.[(triple4)] The mouse is red.[(triple5)] The mouse likes the tiger.[(triple6)] The mouse sees the tiger.[(triple8)] The tiger is red.[(triple9)] The tiger is rough.[(triple10)] The tiger is young.[(triple11)] The tiger likes the cow.[(triple12)] @1: The cow is not blue.[(((triple1) -> rule5))] The mouse does not see the mouse.[(((triple2) -> rule3))] The tiger does not like the tiger.[(((triple10) -> rule2))] @2: The tiger does not like the mouse.[(((triple10 ((triple10) -> rule2)) -> rule7))]
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple2
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
triple3
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple6
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger is young.
("tiger" "is" "young" "+")
triple11
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple12
The cow is not blue.
("cow" "is" "blue" "-")
((triple1) -> (rule5 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
((triple2) -> (rule3 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
((triple10) -> (rule2 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule7 % int1))
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
int1
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int2