The cat chases the lion. The cat is blue. The cat is cold. The cat is green. The cat is round. The cat is young. The cat likes the lion. The cat visits the lion. The lion chases the cat. The lion is cold. The lion is not green. The lion is round. The lion is young. The lion likes the cat. The lion visits the cat. If something is cold then it likes the cat. If something is cold then it visits the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If something is cold then it likes the cat.
((("something" "is" "cold" "+")) -> ("something" "likes" "cat" "+"))
If something is cold then it visits the lion.
((("something" "is" "cold" "+")) -> ("something" "visits" "lion" "+"))
The lion is round.
True
1
proof
[(triple12)]
("lion" "is" "round" "+")
triple12
The cat does not like the lion.
False
1
inv-proof
[(triple7)]
("cat" "likes" "lion" "-")
triple7
The lion visits the lion.
True
2
proof
[(((triple10) -> rule2))]
("lion" "visits" "lion" "+")
((triple10) -> (rule2 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple10) -> rule2))]
("lion" "visits" "lion" "-")
((triple10) -> (rule2 % int1))
The lion visits the lion.
("lion" "visits" "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 blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The cat chases the lion.[(triple1)] The cat is blue.[(triple2)] The cat is cold.[(triple3)] The cat is green.[(triple4)] The cat is round.[(triple5)] The cat is young.[(triple6)] The cat likes the lion.[(triple7)] The cat visits the lion.[(triple8 OR ((triple3) -> rule2))] The lion chases the cat.[(triple9)] The lion is cold.[(triple10)] The lion is not green.[(triple11)] The lion is round.[(triple12)] The lion is young.[(triple13)] The lion likes the cat.[(triple14 OR ((triple10) -> rule1))] The lion visits the cat.[(triple15)] @1: The cat likes the cat.[(((triple3) -> rule1))] The lion visits the lion.[(((triple10) -> rule2))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat is young.
("cat" "is" "young" "+")
triple6
The cat likes the lion.
("cat" "likes" "lion" "+")
triple7
The cat visits the lion.
("cat" "visits" "lion" "+")
triple8
((triple3) -> (rule2 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
triple9
The lion is cold.
("lion" "is" "cold" "+")
triple10
The lion is not green.
("lion" "is" "green" "-")
triple11
The lion is round.
("lion" "is" "round" "+")
triple12
The lion is young.
("lion" "is" "young" "+")
triple13
The lion likes the cat.
("lion" "likes" "cat" "+")
triple14
((triple10) -> (rule1 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
triple15
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple3) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple10) -> (rule2 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1