The cow is red. The cow sees the lion. The dog does not chase the lion. The dog eats the lion. The lion chases the cow. The lion chases the dog. The lion does not chase the rabbit. The lion does not eat the cow. The lion is blue. The lion is not kind. The lion is nice. The lion sees the rabbit. The rabbit does not eat the dog. The rabbit eats the lion. The rabbit is blue. The rabbit sees the cow. If something is nice and not round then it chases the dog. If something eats the lion then it chases the cow. If something chases the cow then it is red. If the rabbit eats the cow and the cow sees the dog then the rabbit eats the lion. If the rabbit is red then the rabbit sees the dog. If the rabbit is not round and the rabbit is not red then the rabbit sees the lion.
The cow is red.
("cow" "is" "red" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The dog does not chase the lion.
("dog" "chases" "lion" "-")
The dog eats the lion.
("dog" "eats" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion does not chase the rabbit.
("lion" "chases" "rabbit" "-")
The lion does not eat the cow.
("lion" "eats" "cow" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit does not eat the dog.
("rabbit" "eats" "dog" "-")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If something is nice and not round then it chases the dog.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "chases" "dog" "+"))
If something eats the lion then it chases the cow.
((("something" "eats" "lion" "+")) -> ("something" "chases" "cow" "+"))
If something chases the cow then it is red.
((("something" "chases" "cow" "+")) -> ("something" "is" "red" "+"))
If the rabbit eats the cow and the cow sees the dog then the rabbit eats the lion.
((("rabbit" "eats" "cow" "+") ("cow" "sees" "dog" "+")) -> ("rabbit" "eats" "lion" "+"))
If the rabbit is red then the rabbit sees the dog.
((("rabbit" "is" "red" "+")) -> ("rabbit" "sees" "dog" "+"))
If the rabbit is not round and the rabbit is not red then the rabbit sees the lion.
((("rabbit" "is" "round" "~") ("rabbit" "is" "red" "~")) -> ("rabbit" "sees" "lion" "+"))
The lion is blue.
True
1
proof
[(triple9)]
("lion" "is" "blue" "+")
triple9
The cow does not see the lion.
False
1
inv-proof
[(triple2)]
("cow" "sees" "lion" "-")
triple2
The rabbit chases the cow.
True
2
proof
[(((triple14) -> rule2))]
("rabbit" "chases" "cow" "+")
((triple14) -> (rule2 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit does not chase the cow.
False
2
inv-proof
[(((triple14) -> rule2))]
("rabbit" "chases" "cow" "-")
((triple14) -> (rule2 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The dog is red.
True
3
proof
[(((((triple4) -> rule2)) -> rule3))]
("dog" "is" "red" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The dog is not red.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule3))]
("dog" "is" "red" "-")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The rabbit sees the dog.
True
4
proof
[(((((((triple14) -> rule2)) -> rule3)) -> rule5))]
("rabbit" "sees" "dog" "+")
((((((triple14) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int3
The rabbit does not see the dog.
False
4
inv-proof
[(((((((triple14) -> rule2)) -> rule3)) -> rule5))]
("rabbit" "sees" "dog" "-")
((((((triple14) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int3
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "dog" "-")
The rabbit chases the dog.
Unknown
rconc
[@1: The rabbit chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "dog" "+")
The cow does not chase the dog.
Unknown
inv-rconc
[@1: The cow chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "dog" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "cow" "+")
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 is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The cow does not eat the lion.
Unknown
inv-random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "-")
The dog sees the cow.
Unknown
random
[@0: The dog sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cow" "+")
@0: The cow is red.[(triple1)] The cow sees the lion.[(triple2)] The dog does not chase the lion.[(triple3)] The dog eats the lion.[(triple4)] The lion chases the cow.[(triple5)] The lion chases the dog.[(triple6)] The lion does not chase the rabbit.[(triple7)] The lion does not eat the cow.[(triple8)] The lion is blue.[(triple9)] The lion is nice.[(triple11)] The lion is not kind.[(triple10)] The lion sees the rabbit.[(triple12)] The rabbit does not eat the dog.[(triple13)] The rabbit eats the lion.[(triple14)] The rabbit is blue.[(triple15)] The rabbit sees the cow.[(triple16)] @1: The dog chases the cow.[(((triple4) -> rule2))] The lion is red.[(((triple5) -> rule3))] The rabbit chases the cow.[(((triple14) -> rule2))] @2: The dog is red.[(((((triple4) -> rule2)) -> rule3))] The rabbit is red.[(((((triple14) -> rule2)) -> rule3))] @3: The rabbit sees the dog.[(((((((triple14) -> rule2)) -> rule3)) -> rule5))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow sees the lion.
("cow" "sees" "lion" "+")
triple2
The dog does not chase the lion.
("dog" "chases" "lion" "-")
triple3
The dog eats the lion.
("dog" "eats" "lion" "+")
triple4
The lion chases the cow.
("lion" "chases" "cow" "+")
triple5
The lion chases the dog.
("lion" "chases" "dog" "+")
triple6
The lion does not chase the rabbit.
("lion" "chases" "rabbit" "-")
triple7
The lion does not eat the cow.
("lion" "eats" "cow" "-")
triple8
The lion is blue.
("lion" "is" "blue" "+")
triple9
The lion is nice.
("lion" "is" "nice" "+")
triple11
The lion is not kind.
("lion" "is" "kind" "-")
triple10
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple12
The rabbit does not eat the dog.
("rabbit" "eats" "dog" "-")
triple13
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple14
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple15
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple16
The dog chases the cow.
("dog" "chases" "cow" "+")
((triple4) -> (rule2 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((triple5) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple14) -> (rule2 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((((triple14) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((((((triple14) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int3