The cat is big. The cow is big. The cow is blue. The cow is nice. The cow needs the lion. The lion eats the cow. The lion likes the cat. If someone is green then they eat the cow. If someone likes the lion then they like the cat. If the cow needs the cat then the cat eats the cow. If someone needs the lion then the lion needs the cow. If someone is big and they need the lion then they like the cow. If someone needs the lion and the lion needs the cow then they like the cat.
The cat is big.
("cat" "is" "big" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
If someone is green then they eat the cow.
((("someone" "is" "green" "+")) -> ("someone" "eats" "cow" "+"))
If someone likes the lion then they like the cat.
((("someone" "likes" "lion" "+")) -> ("someone" "likes" "cat" "+"))
If the cow needs the cat then the cat eats the cow.
((("cow" "needs" "cat" "+")) -> ("cat" "eats" "cow" "+"))
If someone needs the lion then the lion needs the cow.
((("someone" "needs" "lion" "+")) -> ("lion" "needs" "cow" "+"))
If someone is big and they need the lion then they like the cow.
((("someone" "is" "big" "+") ("someone" "needs" "lion" "+")) -> ("someone" "likes" "cow" "+"))
If someone needs the lion and the lion needs the cow then they like the cat.
((("someone" "needs" "lion" "+") ("lion" "needs" "cow" "+")) -> ("someone" "likes" "cat" "+"))
The lion likes the cat.
True
1
proof
[(triple7)]
("lion" "likes" "cat" "+")
triple7
The cow is not big.
False
1
inv-proof
[(triple2)]
("cow" "is" "big" "-")
triple2
The cow likes the cow.
True
3
proof
[(((triple2 triple5) -> rule5))]
("cow" "likes" "cow" "+")
((triple2 triple5) -> (rule5 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow does not like the cow.
False
3
inv-proof
[(((triple2 triple5) -> rule5))]
("cow" "likes" "cow" "-")
((triple2 triple5) -> (rule5 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cat does not eat the cow.
Unknown
inv-rconc
[@1: The cat eats the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "cow" "-")
The lion likes the cow.
Unknown
rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "likes" "cow" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The cow likes the lion.
Unknown
random
[@0: The cow likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "lion" "+")
@0: The cat is big.[(triple1)] The cow is big.[(triple2)] The cow is blue.[(triple3)] The cow is nice.[(triple4)] The cow needs the lion.[(triple5)] The lion eats the cow.[(triple6)] The lion likes the cat.[(triple7)] @1: The cow likes the cow.[(((triple2 triple5) -> rule5))] The lion needs the cow.[(((triple5) -> rule4))] @2: The cow likes the cat.[(((triple5 ((triple5) -> rule4)) -> rule6))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow needs the lion.
("cow" "needs" "lion" "+")
triple5
The lion eats the cow.
("lion" "eats" "cow" "+")
triple6
The lion likes the cat.
("lion" "likes" "cat" "+")
triple7
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple2 triple5) -> (rule5 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
((triple5) -> (rule4 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2