The cat is young. The cow sees the cat. The lion visits the cat. If the cow chases the lion and the lion chases the cow then the lion visits the cat. If the cat visits the lion and the cat chases the lion then the cat is red. If something chases the cow and it does not see the cow then the cow is not nice. If the cow chases the lion then the cow is young. If something is red and it does not chase the cow then it is not young. If something sees the cat then it is not red. If something is young then it visits the cow. If something visits the lion then it sees the lion.
The cat is young.
("cat" "is" "young" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If the cow chases the lion and the lion chases the cow then the lion visits the cat.
((("cow" "chases" "lion" "+") ("lion" "chases" "cow" "+")) -> ("lion" "visits" "cat" "+"))
If the cat visits the lion and the cat chases the lion then the cat is red.
((("cat" "visits" "lion" "+") ("cat" "chases" "lion" "+")) -> ("cat" "is" "red" "+"))
If something chases the cow and it does not see the cow then the cow is not nice.
((("something" "chases" "cow" "+") ("something" "sees" "cow" "~")) -> ("cow" "is" "nice" "-"))
If the cow chases the lion then the cow is young.
((("cow" "chases" "lion" "+")) -> ("cow" "is" "young" "+"))
If something is red and it does not chase the cow then it is not young.
((("something" "is" "red" "+") ("something" "chases" "cow" "~")) -> ("something" "is" "young" "-"))
If something sees the cat then it is not red.
((("something" "sees" "cat" "+")) -> ("something" "is" "red" "-"))
If something is young then it visits the cow.
((("something" "is" "young" "+")) -> ("something" "visits" "cow" "+"))
If something visits the lion then it sees the lion.
((("something" "visits" "lion" "+")) -> ("something" "sees" "lion" "+"))
The cat is young.
True
1
proof
[(triple1)]
("cat" "is" "young" "+")
triple1
The cow does not see the cat.
False
1
inv-proof
[(triple2)]
("cow" "sees" "cat" "-")
triple2
The cow is not red.
True
2
proof
[(((triple2) -> rule6))]
("cow" "is" "red" "-")
((triple2) -> (rule6 % int1))
The cow is not red.
("cow" "is" "red" "-")
int1
The cow is red.
False
2
inv-proof
[(((triple2) -> rule6))]
("cow" "is" "red" "+")
((triple2) -> (rule6 % int1))
The cow is not red.
("cow" "is" "red" "-")
int1
The cow does not see the lion.
Unknown
inv-rconc
[@1: The cow sees the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "sees" "lion" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "young" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The cat visits the lion.
Unknown
random
[@0: The cat visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "lion" "+")
@0: The cat is young.[(triple1)] The cow sees the cat.[(triple2)] The lion visits the cat.[(triple3)] @1: The cat visits the cow.[(((triple1) -> rule7))] The cow is not red.[(((triple2) -> rule6))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cow sees the cat.
("cow" "sees" "cat" "+")
triple2
The lion visits the cat.
("lion" "visits" "cat" "+")
triple3
The cat visits the cow.
("cat" "visits" "cow" "+")
((triple1) -> (rule7 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cow is not red.
("cow" "is" "red" "-")
((triple2) -> (rule6 % int1))
The cow is not red.
("cow" "is" "red" "-")
int1