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