The cow needs the lion. The lion sees the cow. If something needs the lion and it is young then the lion sees the cow. If something needs the cow then it likes the lion. If something likes the cow then it sees the lion. If something needs the cow then it likes the cow. If something likes the lion then the lion needs the cow. If something sees the cow and the cow likes the lion then the lion is green. If the cow sees the lion and the cow is nice then the lion is nice. If something sees the cow then it needs the cow.
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If something needs the lion and it is young then the lion sees the cow.
((("something" "needs" "lion" "+") ("something" "is" "young" "+")) -> ("lion" "sees" "cow" "+"))
If something needs the cow then it likes the lion.
((("something" "needs" "cow" "+")) -> ("something" "likes" "lion" "+"))
If something likes the cow then it sees the lion.
((("something" "likes" "cow" "+")) -> ("something" "sees" "lion" "+"))
If something needs the cow then it likes the cow.
((("something" "needs" "cow" "+")) -> ("something" "likes" "cow" "+"))
If something likes the lion then the lion needs the cow.
((("something" "likes" "lion" "+")) -> ("lion" "needs" "cow" "+"))
If something sees the cow and the cow likes the lion then the lion is green.
((("something" "sees" "cow" "+") ("cow" "likes" "lion" "+")) -> ("lion" "is" "green" "+"))
If the cow sees the lion and the cow is nice then the lion is nice.
((("cow" "sees" "lion" "+") ("cow" "is" "nice" "+")) -> ("lion" "is" "nice" "+"))
If something sees the cow then it needs the cow.
((("something" "sees" "cow" "+")) -> ("something" "needs" "cow" "+"))
The lion sees the cow.
True
1
proof
[(triple2)]
("lion" "sees" "cow" "+")
triple2
The lion does not see the cow.
False
1
inv-proof
[(triple2)]
("lion" "sees" "cow" "-")
triple2
The lion needs the cow.
True
2
proof
[(((triple2) -> rule8))]
("lion" "needs" "cow" "+")
((triple2) -> (rule8 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion does not need the cow.
False
2
inv-proof
[(((triple2) -> rule8))]
("lion" "needs" "cow" "-")
((triple2) -> (rule8 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion likes the lion.
True
3
proof
[(((((triple2) -> rule8)) -> rule2))]
("lion" "likes" "lion" "+")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion does not like the lion.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule2))]
("lion" "likes" "lion" "-")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion sees the lion.
True
4
proof
[(((((((triple2) -> rule8)) -> rule4)) -> rule3))]
("lion" "sees" "lion" "+")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion needs the cow.
("lion" "needs" "cow" "+")
int3
The lion does not see the lion.
False
4
inv-proof
[(((((((triple2) -> rule8)) -> rule4)) -> rule3))]
("lion" "sees" "lion" "-")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion needs the cow.
("lion" "needs" "cow" "+")
int3
The cow does not like the lion.
Unknown
inv-rconc
[@2: The cow likes the lion.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("cow" "likes" "lion" "-")
The cow sees the lion.
Unknown
rconc
[@3: The cow sees the lion.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule8 <- FAIL)]]
("cow" "sees" "lion" "+")
The lion is not green.
Unknown
inv-rconc
[@3: The lion is green.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule8 <- FAIL)]]
("lion" "is" "green" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "is" "nice" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow needs the lion.[(triple1)] The lion sees the cow.[(triple2)] @1: The lion needs the cow.[(((triple2) -> rule8))] @2: The lion likes the cow.[(((((triple2) -> rule8)) -> rule4))] The lion likes the lion.[(((((triple2) -> rule8)) -> rule2))] @3: The lion sees the lion.[(((((((triple2) -> rule8)) -> rule4)) -> rule3))]
The cow needs the lion.
("cow" "needs" "lion" "+")
triple1
The lion sees the cow.
("lion" "sees" "cow" "+")
triple2
The lion needs the cow.
("lion" "needs" "cow" "+")
((triple2) -> (rule8 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion needs the cow.
("lion" "needs" "cow" "+")
int3