The cat chases the mouse. The cat visits the mouse. The cat visits the tiger. The mouse sees the cat. The mouse visits the cat. The tiger chases the cat. The tiger is green. The tiger is red. The tiger sees the cat. The tiger visits the cat. If the cat is cold then the cat sees the tiger. If something visits the cat and it chases the mouse then it visits the tiger. If the mouse chases the cat and the mouse visits the tiger then the cat chases the tiger. If the tiger is round then the tiger chases the mouse. If something is red and it chases the tiger then it chases the cat. If something visits the cat then it chases the mouse. If something sees the mouse then it visits the tiger. If something is rough and it chases the tiger then it sees the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If the cat is cold then the cat sees the tiger.
((("cat" "is" "cold" "+")) -> ("cat" "sees" "tiger" "+"))
If something visits the cat and it chases the mouse then it visits the tiger.
((("something" "visits" "cat" "+") ("something" "chases" "mouse" "+")) -> ("something" "visits" "tiger" "+"))
If the mouse chases the cat and the mouse visits the tiger then the cat chases the tiger.
((("mouse" "chases" "cat" "+") ("mouse" "visits" "tiger" "+")) -> ("cat" "chases" "tiger" "+"))
If the tiger is round then the tiger chases the mouse.
((("tiger" "is" "round" "+")) -> ("tiger" "chases" "mouse" "+"))
If something is red and it chases the tiger then it chases the cat.
((("something" "is" "red" "+") ("something" "chases" "tiger" "+")) -> ("something" "chases" "cat" "+"))
If something visits the cat then it chases the mouse.
((("something" "visits" "cat" "+")) -> ("something" "chases" "mouse" "+"))
If something sees the mouse then it visits the tiger.
((("something" "sees" "mouse" "+")) -> ("something" "visits" "tiger" "+"))
If something is rough and it chases the tiger then it sees the mouse.
((("something" "is" "rough" "+") ("something" "chases" "tiger" "+")) -> ("something" "sees" "mouse" "+"))
The tiger chases the cat.
True
1
proof
[(triple6)]
("tiger" "chases" "cat" "+")
triple6
The tiger is not red.
False
1
inv-proof
[(triple8)]
("tiger" "is" "red" "-")
triple8
The mouse chases the mouse.
True
2
proof
[(((triple5) -> rule6))]
("mouse" "chases" "mouse" "+")
((triple5) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
2
inv-proof
[(((triple5) -> rule6))]
("mouse" "chases" "mouse" "-")
((triple5) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the tiger.
True
4
proof
[(((triple5 ((triple5) -> rule6)) -> rule2))]
("mouse" "visits" "tiger" "+")
((triple5 ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse does not visit the tiger.
False
4
inv-proof
[(((triple5 ((triple5) -> rule6)) -> rule2))]
("mouse" "visits" "tiger" "-")
((triple5 ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The cat does not see the tiger.
Unknown
inv-rconc
[@1: The cat sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "tiger" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "chases" "cat" "+")
The mouse does not chase the cat.
Unknown
inv-rconc
[@1: The mouse chases the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "cat" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cat chases the mouse.[(triple1)] The cat visits the mouse.[(triple2)] The cat visits the tiger.[(triple3)] The mouse sees the cat.[(triple4)] The mouse visits the cat.[(triple5)] The tiger chases the cat.[(triple6)] The tiger is green.[(triple7)] The tiger is red.[(triple8)] The tiger sees the cat.[(triple9)] The tiger visits the cat.[(triple10)] @1: The mouse chases the mouse.[(((triple5) -> rule6))] The tiger chases the mouse.[(((triple10) -> rule6))] @2: The mouse visits the tiger.[(((triple5 ((triple5) -> rule6)) -> rule2))] The tiger visits the tiger.[(((triple10 ((triple10) -> rule6)) -> rule2))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple4
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple5
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The tiger is red.
("tiger" "is" "red" "+")
triple8
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple9
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple5) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((triple10) -> (rule6 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
((triple5 ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple10 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2