The cow eats the lion. The cow is not blue. The cow is green. The cow is red. The cow needs the lion. The cow sees the lion. The lion does not eat the cow. The lion is big. The lion is red. The lion needs the cow. If something is red and it does not need the lion then it does not eat the lion. If something is big then it eats the lion. If something is green and it does not need the cow then the cow eats the lion. If something sees the lion and it is not green then the lion eats the cow. If the lion is not big then the lion sees the cow. If something is round and green then it does not see the lion. If something needs the cow and the cow is red then it sees the cow. If something sees the cow then it is not blue.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow is green.
("cow" "is" "green" "+")
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 does not eat the cow.
("lion" "eats" "cow" "-")
The lion is big.
("lion" "is" "big" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
If something is red and it does not need the lion then it does not eat the lion.
((("something" "is" "red" "+") ("something" "needs" "lion" "~")) -> ("something" "eats" "lion" "-"))
If something is big then it eats the lion.
((("something" "is" "big" "+")) -> ("something" "eats" "lion" "+"))
If something is green and it does not need the cow then the cow eats the lion.
((("something" "is" "green" "+") ("something" "needs" "cow" "~")) -> ("cow" "eats" "lion" "+"))
If something sees the lion and it is not green then the lion eats the cow.
((("something" "sees" "lion" "+") ("something" "is" "green" "~")) -> ("lion" "eats" "cow" "+"))
If the lion is not big then the lion sees the cow.
((("lion" "is" "big" "~")) -> ("lion" "sees" "cow" "+"))
If something is round and green then it does not see the lion.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "sees" "lion" "-"))
If something needs the cow and the cow is red then it sees the cow.
((("something" "needs" "cow" "+") ("cow" "is" "red" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow then it is not blue.
((("something" "sees" "cow" "+")) -> ("something" "is" "blue" "-"))
The cow is green.
True
1
proof
[(triple3)]
("cow" "is" "green" "+")
triple3
The cow does not need the lion.
False
1
inv-proof
[(triple5)]
("cow" "needs" "lion" "-")
triple5
The lion sees the cow.
True
3
proof
[(((triple10 triple4) -> rule7))]
("lion" "sees" "cow" "+")
((triple10 triple4) -> (rule7 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion does not eat the lion.
False
2
inv-proof
[(((triple8) -> rule2))]
("lion" "eats" "lion" "-")
((triple8) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is not blue.
True
4
proof
[(((((triple10 triple4) -> rule7)) -> rule8))]
("lion" "is" "blue" "-")
((((triple10 triple4) -> (rule7 % int2))) -> (rule8 % int1))
The lion is not blue.
("lion" "is" "blue" "-")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is blue.
False
4
inv-proof
[(((((triple10 triple4) -> rule7)) -> rule8))]
("lion" "is" "blue" "+")
((((triple10 triple4) -> (rule7 % int2))) -> (rule8 % int1))
The lion is not blue.
("lion" "is" "blue" "-")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "sees" "cow" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "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 eats the lion.[(triple1)] The cow is green.[(triple3)] The cow is not blue.[(triple2)] The cow is red.[(triple4)] The cow needs the lion.[(triple5)] The cow sees the lion.[(triple6)] The lion does not eat the cow.[(triple7)] The lion is big.[(triple8)] The lion is red.[(triple9)] The lion needs the cow.[(triple10)] @1: The lion eats the lion.[(((triple8) -> rule2))] The lion sees the cow.[(((triple10 triple4) -> rule7))] @2: The lion is not blue.[(((((triple10 triple4) -> rule7)) -> rule8))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is not blue.
("cow" "is" "blue" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple4
The cow needs the lion.
("cow" "needs" "lion" "+")
triple5
The cow sees the lion.
("cow" "sees" "lion" "+")
triple6
The lion does not eat the cow.
("lion" "eats" "cow" "-")
triple7
The lion is big.
("lion" "is" "big" "+")
triple8
The lion is red.
("lion" "is" "red" "+")
triple9
The lion needs the cow.
("lion" "needs" "cow" "+")
triple10
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple8) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple10 triple4) -> (rule7 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is not blue.
("lion" "is" "blue" "-")
((((triple10 triple4) -> (rule7 % int2))) -> (rule8 % int1))
The lion is not blue.
("lion" "is" "blue" "-")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2