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