The cat is cold. The cow chases the lion. The lion eats the cow. If the lion is cold and the lion eats the cow then the cow eats the lion. If the lion eats the cow and the lion chases the cat then the cow is red. If the cat is cold then the cat likes the cow. If someone is young and they chase the cat then they are kind. If the cat chases the lion and the lion is young then the cat is red. If someone chases the lion then the lion chases the cat. If someone is red then they chase the cow. If the cow chases the cat then the cow is kind.
The cat is cold.
("cat" "is" "cold" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
If the lion is cold and the lion eats the cow then the cow eats the lion.
((("lion" "is" "cold" "+") ("lion" "eats" "cow" "+")) -> ("cow" "eats" "lion" "+"))
If the lion eats the cow and the lion chases the cat then the cow is red.
((("lion" "eats" "cow" "+") ("lion" "chases" "cat" "+")) -> ("cow" "is" "red" "+"))
If the cat is cold then the cat likes the cow.
((("cat" "is" "cold" "+")) -> ("cat" "likes" "cow" "+"))
If someone is young and they chase the cat then they are kind.
((("someone" "is" "young" "+") ("someone" "chases" "cat" "+")) -> ("someone" "is" "kind" "+"))
If the cat chases the lion and the lion is young then the cat is red.
((("cat" "chases" "lion" "+") ("lion" "is" "young" "+")) -> ("cat" "is" "red" "+"))
If someone chases the lion then the lion chases the cat.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "cat" "+"))
If someone is red then they chase the cow.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cow" "+"))
If the cow chases the cat then the cow is kind.
((("cow" "chases" "cat" "+")) -> ("cow" "is" "kind" "+"))
The cat is cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "+")
triple1
The cat is not cold.
False
1
inv-proof
[(triple1)]
("cat" "is" "cold" "-")
triple1
The lion chases the cat.
True
2
proof
[(((triple2) -> rule6))]
("lion" "chases" "cat" "+")
((triple2) -> (rule6 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion does not chase the cat.
False
2
inv-proof
[(((triple2) -> rule6))]
("lion" "chases" "cat" "-")
((triple2) -> (rule6 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The cow is red.
True
4
proof
[(((triple3 ((triple2) -> rule6)) -> rule2))]
("cow" "is" "red" "+")
((triple3 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The cow is not red.
False
4
inv-proof
[(((triple3 ((triple2) -> rule6)) -> rule2))]
("cow" "is" "red" "-")
((triple3 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The cow chases the cow.
True
5
proof
[(((((triple3 ((triple2) -> rule6)) -> rule2)) -> rule7))]
("cow" "chases" "cow" "+")
((((triple3 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3
The cow does not chase the cow.
False
5
inv-proof
[(((((triple3 ((triple2) -> rule6)) -> rule2)) -> rule7))]
("cow" "chases" "cow" "-")
((((triple3 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3
The cat does not chase the cow.
Unknown
inv-rconc
[@2: The cat chases the cow.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("cat" "chases" "cow" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "red" "+")
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "kind" "-")
The lion chases the cow.
Unknown
rconc
[@1: The lion chases the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "chases" "cow" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The cat is cold.[(triple1)] The cow chases the lion.[(triple2)] The lion eats the cow.[(triple3)] @1: The cat likes the cow.[(((triple1) -> rule3))] The lion chases the cat.[(((triple2) -> rule6))] @2: The cow is red.[(((triple3 ((triple2) -> rule6)) -> rule2))] @3: The cow chases the cow.[(((((triple3 ((triple2) -> rule6)) -> rule2)) -> rule7))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cow chases the lion.
("cow" "chases" "lion" "+")
triple2
The lion eats the cow.
("lion" "eats" "cow" "+")
triple3
The cat likes the cow.
("cat" "likes" "cow" "+")
((triple1) -> (rule3 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
((triple2) -> (rule6 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((triple3 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((((triple3 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3