The cat eats the lion. The cat is blue. The cat is red. The cat is rough. The cat is young. The cat likes the cow. The cat likes the lion. The cat sees the cow. The cow eats the cat. The cow is young. The cow sees the lion. The lion eats the cat. The lion is young. The lion likes the cow. The lion sees the cat. The lion sees the cow. If someone eats the cat then they are not blue. If someone eats the lion then they eat the cow.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If someone eats the cat then they are not blue.
((("someone" "eats" "cat" "+")) -> ("someone" "is" "blue" "-"))
If someone eats the lion then they eat the cow.
((("someone" "eats" "lion" "+")) -> ("someone" "eats" "cow" "+"))
The cat eats the lion.
True
1
proof
[(triple1)]
("cat" "eats" "lion" "+")
triple1
The cow does not see the lion.
False
1
inv-proof
[(triple11)]
("cow" "sees" "lion" "-")
triple11
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "cow" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The cat eats the lion.[(triple1)] The cat is blue.[(triple2)] The cat is red.[(triple3)] The cat is rough.[(triple4)] The cat is young.[(triple5)] The cat likes the cow.[(triple6)] The cat likes the lion.[(triple7)] The cat sees the cow.[(triple8)] The cow eats the cat.[(triple9)] The cow is young.[(triple10)] The cow sees the lion.[(triple11)] The lion eats the cat.[(triple12)] The lion is young.[(triple13)] The lion likes the cow.[(triple14)] The lion sees the cat.[(triple15)] The lion sees the cow.[(triple16)] @1: The cat eats the cow.[(((triple1) -> rule2))] The cow is not blue.[(((triple9) -> rule1))] The lion is not blue.[(((triple12) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the cow.
("cat" "likes" "cow" "+")
triple6
The cat likes the lion.
("cat" "likes" "lion" "+")
triple7
The cat sees the cow.
("cat" "sees" "cow" "+")
triple8
The cow eats the cat.
("cow" "eats" "cat" "+")
triple9
The cow is young.
("cow" "is" "young" "+")
triple10
The cow sees the lion.
("cow" "sees" "lion" "+")
triple11
The lion eats the cat.
("lion" "eats" "cat" "+")
triple12
The lion is young.
("lion" "is" "young" "+")
triple13
The lion likes the cow.
("lion" "likes" "cow" "+")
triple14
The lion sees the cat.
("lion" "sees" "cat" "+")
triple15
The lion sees the cow.
("lion" "sees" "cow" "+")
triple16
The cat eats the cow.
("cat" "eats" "cow" "+")
((triple1) -> (rule2 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cow is not blue.
("cow" "is" "blue" "-")
((triple9) -> (rule1 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The lion is not blue.
("lion" "is" "blue" "-")
((triple12) -> (rule1 % int1))
The lion is not blue.
("lion" "is" "blue" "-")
int1