The cow sees the lion. The lion is not big. If someone needs the cow and the cow is big then the cow is nice. If someone is blue then they are big. If someone sees the lion then the lion is nice. If the lion is blue and the lion is big then the lion likes the cow. If someone needs the lion then they do not like the lion. If someone is nice then they need the lion. If the cow is cold and the cow is not blue then the cow is not big. If the lion is cold and the lion is not nice then the lion sees the cow.
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion is not big.
("lion" "is" "big" "-")
If someone needs the cow and the cow is big then the cow is nice.
((("someone" "needs" "cow" "+") ("cow" "is" "big" "+")) -> ("cow" "is" "nice" "+"))
If someone is blue then they are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone sees the lion then the lion is nice.
((("someone" "sees" "lion" "+")) -> ("lion" "is" "nice" "+"))
If the lion is blue and the lion is big then the lion likes the cow.
((("lion" "is" "blue" "+") ("lion" "is" "big" "+")) -> ("lion" "likes" "cow" "+"))
If someone needs the lion then they do not like the lion.
((("someone" "needs" "lion" "+")) -> ("someone" "likes" "lion" "-"))
If someone is nice then they need the lion.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "lion" "+"))
If the cow is cold and the cow is not blue then the cow is not big.
((("cow" "is" "cold" "+") ("cow" "is" "blue" "~")) -> ("cow" "is" "big" "-"))
If the lion is cold and the lion is not nice then the lion sees the cow.
((("lion" "is" "cold" "+") ("lion" "is" "nice" "~")) -> ("lion" "sees" "cow" "+"))
The cow sees the lion.
True
1
proof
[(triple1)]
("cow" "sees" "lion" "+")
triple1
The cow does not see the lion.
False
1
inv-proof
[(triple1)]
("cow" "sees" "lion" "-")
triple1
The lion is nice.
True
2
proof
[(((triple1) -> rule3))]
("lion" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("lion" "is" "nice" "-")
((triple1) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion needs the lion.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("lion" "needs" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("lion" "needs" "lion" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion does not like the lion.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule5))]
("lion" "likes" "lion" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion does not like the lion.
("lion" "likes" "lion" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion likes the lion.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule5))]
("lion" "likes" "lion" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion does not like the lion.
("lion" "likes" "lion" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion does not see the cow.
Unknown
inv-rconc
[@1: The lion sees the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "sees" "cow" "-")
The lion likes the cow.
Unknown
rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "likes" "cow" "+")
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "big" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "nice" "+")
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 cow likes the lion.
Unknown
random
[@0: The cow likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "lion" "+")
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 cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow sees the lion.[(triple1)] The lion is not big.[(triple2)] @1: The lion is nice.[(((triple1) -> rule3))] @2: The lion needs the lion.[(((((triple1) -> rule3)) -> rule6))] @3: The lion does not like the lion.[(((((((triple1) -> rule3)) -> rule6)) -> rule5))]
The cow sees the lion.
("cow" "sees" "lion" "+")
triple1
The lion is not big.
("lion" "is" "big" "-")
triple2
The lion is nice.
("lion" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion does not like the lion.
("lion" "likes" "lion" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion does not like the lion.
("lion" "likes" "lion" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3