The cat chases the cow. The cat visits the cow. The cat visits the lion. The cat visits the mouse. The cow is red. The lion is big. The lion visits the cow. The mouse chases the cat. The mouse chases the cow. The mouse is nice. The mouse is red. The mouse visits the cat. If something visits the cat then it chases the lion.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cow is red.
("cow" "is" "red" "+")
The lion is big.
("lion" "is" "big" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If something visits the cat then it chases the lion.
((("something" "visits" "cat" "+")) -> ("something" "chases" "lion" "+"))
The lion visits the cow.
True
1
proof
[(triple7)]
("lion" "visits" "cow" "+")
triple7
The mouse does not chase the cat.
False
1
inv-proof
[(triple8)]
("mouse" "chases" "cat" "-")
triple8
The mouse chases the lion.
True
2
proof
[(((triple12) -> rule1))]
("mouse" "chases" "lion" "+")
((triple12) -> (rule1 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse does not chase the lion.
False
2
inv-proof
[(((triple12) -> rule1))]
("mouse" "chases" "lion" "-")
((triple12) -> (rule1 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The cow does not chase the lion.
Unknown
inv-rconc
[@1: The cow chases the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "lion" "-")
The cat chases the lion.
Unknown
rconc
[@1: The cat chases the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "lion" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cat chases the cow.[(triple1)] The cat visits the cow.[(triple2)] The cat visits the lion.[(triple3)] The cat visits the mouse.[(triple4)] The cow is red.[(triple5)] The lion is big.[(triple6)] The lion visits the cow.[(triple7)] The mouse chases the cat.[(triple8)] The mouse chases the cow.[(triple9)] The mouse is nice.[(triple10)] The mouse is red.[(triple11)] The mouse visits the cat.[(triple12)] @1: The mouse chases the lion.[(((triple12) -> rule1))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat visits the cow.
("cat" "visits" "cow" "+")
triple2
The cat visits the lion.
("cat" "visits" "lion" "+")
triple3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple4
The cow is red.
("cow" "is" "red" "+")
triple5
The lion is big.
("lion" "is" "big" "+")
triple6
The lion visits the cow.
("lion" "visits" "cow" "+")
triple7
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple9
The mouse is nice.
("mouse" "is" "nice" "+")
triple10
The mouse is red.
("mouse" "is" "red" "+")
triple11
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple12
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((triple12) -> (rule1 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1