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