The cow eats the lion. The cow is not kind. The cow is red. The cow needs the lion. The cow sees the lion. The lion is not kind. The lion is rough. The lion is round. The lion is young. The lion needs the cow. If the cow is red and the lion does not need the cow then the lion is round. If someone is rough and they see the cow then the cow needs the lion. If someone is rough and not red then they are kind. If the cow eats the lion then the lion eats the cow. If the cow eats the lion and the lion eats the cow then the cow is rough. If someone is round then they do not eat the lion.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is not kind.
("cow" "is" "kind" "-")
The cow is red.
("cow" "is" "red" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
If the cow is red and the lion does not need the cow then the lion is round.
((("cow" "is" "red" "+") ("lion" "needs" "cow" "~")) -> ("lion" "is" "round" "+"))
If someone is rough and they see the cow then the cow needs the lion.
((("someone" "is" "rough" "+") ("someone" "sees" "cow" "+")) -> ("cow" "needs" "lion" "+"))
If someone is rough and not red then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "kind" "+"))
If the cow eats the lion then the lion eats the cow.
((("cow" "eats" "lion" "+")) -> ("lion" "eats" "cow" "+"))
If the cow eats the lion and the lion eats the cow then the cow is rough.
((("cow" "eats" "lion" "+") ("lion" "eats" "cow" "+")) -> ("cow" "is" "rough" "+"))
If someone is round then they do not eat the lion.
((("someone" "is" "round" "+")) -> ("someone" "eats" "lion" "-"))
The lion needs the cow.
True
1
proof
[(triple10)]
("lion" "needs" "cow" "+")
triple10
The cow is kind.
False
1
inv-proof
[(triple2)]
("cow" "is" "kind" "+")
triple2
The lion eats the cow.
True
2
proof
[(((triple1) -> rule4))]
("lion" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion eats the lion.
False
2
inv-proof
[(((triple8) -> rule6))]
("lion" "eats" "lion" "+")
((triple8) -> (rule6 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The cow is rough.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule5))]
("cow" "is" "rough" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The cow is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule5))]
("cow" "is" "rough" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The lion does not see the cow.
Unknown
inv-random
[@0: The lion sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow eats the lion.[(triple1)] The cow is not kind.[(triple2)] The cow is red.[(triple3)] The cow needs the lion.[(triple4)] The cow sees the lion.[(triple5)] The lion is not kind.[(triple6)] The lion is rough.[(triple7)] The lion is round.[(triple8)] The lion is young.[(triple9)] The lion needs the cow.[(triple10)] @1: The lion does not eat the lion.[(((triple8) -> rule6))] The lion eats the cow.[(((triple1) -> rule4))] @2: The cow is rough.[(((triple1 ((triple1) -> rule4)) -> rule5))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is not kind.
("cow" "is" "kind" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow needs the lion.
("cow" "needs" "lion" "+")
triple4
The cow sees the lion.
("cow" "sees" "lion" "+")
triple5
The lion is not kind.
("lion" "is" "kind" "-")
triple6
The lion is rough.
("lion" "is" "rough" "+")
triple7
The lion is round.
("lion" "is" "round" "+")
triple8
The lion is young.
("lion" "is" "young" "+")
triple9
The lion needs the cow.
("lion" "needs" "cow" "+")
triple10
The lion does not eat the lion.
("lion" "eats" "lion" "-")
((triple8) -> (rule6 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2