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