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