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