The cow is round. The cow needs the lion. The lion is round. If someone chases the cow and the cow chases the lion then they are big. If someone likes the lion then the lion is red. If the cow is round then the cow likes the lion. If someone is rough and not kind then they chase the cow. All rough people are not red. If someone is round then they do not need the cow. If the cow does not like the lion and the lion does not need the cow then the cow is red. If someone is red then they do not like the cow.
The cow is round.
("cow" "is" "round" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion is round.
("lion" "is" "round" "+")
If someone chases the cow and the cow chases the lion then they are big.
((("someone" "chases" "cow" "+") ("cow" "chases" "lion" "+")) -> ("someone" "is" "big" "+"))
If someone likes the lion then the lion is red.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "red" "+"))
If the cow is round then the cow likes the lion.
((("cow" "is" "round" "+")) -> ("cow" "likes" "lion" "+"))
If someone is rough and not kind then they chase the cow.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "~")) -> ("someone" "chases" "cow" "+"))
All rough people are not red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "-"))
If someone is round then they do not need the cow.
((("someone" "is" "round" "+")) -> ("someone" "needs" "cow" "-"))
If the cow does not like the lion and the lion does not need the cow then the cow is red.
((("cow" "likes" "lion" "~") ("lion" "needs" "cow" "~")) -> ("cow" "is" "red" "+"))
If someone is red then they do not like the cow.
((("someone" "is" "red" "+")) -> ("someone" "likes" "cow" "-"))
The lion is round.
True
1
proof
[(triple3)]
("lion" "is" "round" "+")
triple3
The cow is not round.
False
1
inv-proof
[(triple1)]
("cow" "is" "round" "-")
triple1
The cow likes the lion.
True
2
proof
[(((triple1) -> rule3))]
("cow" "likes" "lion" "+")
((triple1) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow needs the cow.
False
2
inv-proof
[(((triple1) -> rule6))]
("cow" "needs" "cow" "+")
((triple1) -> (rule6 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The lion is red.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("lion" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The lion is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("lion" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The lion does not like the cow.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule8))]
("lion" "likes" "cow" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion does not like the cow.
("lion" "likes" "cow" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
int3
The lion likes the cow.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule8))]
("lion" "likes" "cow" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion does not like the cow.
("lion" "likes" "cow" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
int3
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "red" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cow" "+")
The lion does not chase the cow.
Unknown
inv-rconc
[@1: The lion chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "chases" "cow" "-")
The cow is big.
Unknown
rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "big" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cow chases the lion.
Unknown
random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "+")
@0: The cow is round.[(triple1)] The cow needs the lion.[(triple2)] The lion is round.[(triple3)] @1: The cow does not need the cow.[(((triple1) -> rule6))] The cow likes the lion.[(((triple1) -> rule3))] The lion does not need the cow.[(((triple3) -> rule6))] @2: The lion is red.[(((((triple1) -> rule3)) -> rule2))] @3: The lion does not like the cow.[(((((((triple1) -> rule3)) -> rule2)) -> rule8))]
The cow is round.
("cow" "is" "round" "+")
triple1
The cow needs the lion.
("cow" "needs" "lion" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The cow does not need the cow.
("cow" "needs" "cow" "-")
((triple1) -> (rule6 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
((triple1) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The lion does not need the cow.
("lion" "needs" "cow" "-")
((triple3) -> (rule6 % int1))
The lion does not need the cow.
("lion" "needs" "cow" "-")
int1
The lion is red.
("lion" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The lion does not like the cow.
("lion" "likes" "cow" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion does not like the cow.
("lion" "likes" "cow" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
int3