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