The cow sees the lion. The lion eats the cow. The rabbit needs the cow. If something sees the rabbit and the rabbit is cold then the rabbit is big. If something needs the rabbit and the rabbit does not eat the cow then it is kind. If the lion eats the rabbit then the lion is big. If something sees the lion then the lion eats the rabbit. If something sees the lion and it needs the rabbit then the rabbit does not see the lion. If something is blue then it sees the cow. If something eats the cow and it is young then it sees the rabbit. If something is blue and it does not see the rabbit then it does not need the lion.
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If something sees the rabbit and the rabbit is cold then the rabbit is big.
((("something" "sees" "rabbit" "+") ("rabbit" "is" "cold" "+")) -> ("rabbit" "is" "big" "+"))
If something needs the rabbit and the rabbit does not eat the cow then it is kind.
((("something" "needs" "rabbit" "+") ("rabbit" "eats" "cow" "~")) -> ("something" "is" "kind" "+"))
If the lion eats the rabbit then the lion is big.
((("lion" "eats" "rabbit" "+")) -> ("lion" "is" "big" "+"))
If something sees the lion then the lion eats the rabbit.
((("something" "sees" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If something sees the lion and it needs the rabbit then the rabbit does not see the lion.
((("something" "sees" "lion" "+") ("something" "needs" "rabbit" "+")) -> ("rabbit" "sees" "lion" "-"))
If something is blue then it sees the cow.
((("something" "is" "blue" "+")) -> ("something" "sees" "cow" "+"))
If something eats the cow and it is young then it sees the rabbit.
((("something" "eats" "cow" "+") ("something" "is" "young" "+")) -> ("something" "sees" "rabbit" "+"))
If something is blue and it does not see the rabbit then it does not need the lion.
((("something" "is" "blue" "+") ("something" "sees" "rabbit" "~")) -> ("something" "needs" "lion" "-"))
The lion eats the cow.
True
1
proof
[(triple2)]
("lion" "eats" "cow" "+")
triple2
The rabbit does not need the cow.
False
1
inv-proof
[(triple3)]
("rabbit" "needs" "cow" "-")
triple3
The lion eats the rabbit.
True
2
proof
[(((triple1) -> rule4))]
("lion" "eats" "rabbit" "+")
((triple1) -> (rule4 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion does not eat the rabbit.
False
2
inv-proof
[(((triple1) -> rule4))]
("lion" "eats" "rabbit" "-")
((triple1) -> (rule4 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion is big.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("lion" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The lion is not big.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("lion" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The lion does not see the cow.
Unknown
inv-rconc
[@1: The lion sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "sees" "cow" "-")
The lion sees the rabbit.
Unknown
rconc
[@1: The lion sees the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "rabbit" "+")
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "kind" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
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 lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The cow sees the lion.[(triple1)] The lion eats the cow.[(triple2)] The rabbit needs the cow.[(triple3)] @1: The lion eats the rabbit.[(((triple1) -> rule4))] @2: The lion is big.[(((((triple1) -> rule4)) -> rule3))]
The cow sees the lion.
("cow" "sees" "lion" "+")
triple1
The lion eats the cow.
("lion" "eats" "cow" "+")
triple2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((triple1) -> (rule4 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2