The cat is blue. The cow likes the lion. The lion likes the cow. If something likes the cow and it chases the cow then it is red. If something is kind then it needs the lion. If something needs the cat then it chases the lion. If something likes the lion and the lion likes the cow then the lion needs the cow. All big things are cold. If something likes the cow and the cow needs the lion then it chases the cat. If something likes the cow then it needs the cat. If the lion likes the cat and the cat needs the cow then the cow is cold.
The cat is blue.
("cat" "is" "blue" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
If something likes the cow and it chases the cow then it is red.
((("something" "likes" "cow" "+") ("something" "chases" "cow" "+")) -> ("something" "is" "red" "+"))
If something is kind then it needs the lion.
((("something" "is" "kind" "+")) -> ("something" "needs" "lion" "+"))
If something needs the cat then it chases the lion.
((("something" "needs" "cat" "+")) -> ("something" "chases" "lion" "+"))
If something likes the lion and the lion likes the cow then the lion needs the cow.
((("something" "likes" "lion" "+") ("lion" "likes" "cow" "+")) -> ("lion" "needs" "cow" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something likes the cow and the cow needs the lion then it chases the cat.
((("something" "likes" "cow" "+") ("cow" "needs" "lion" "+")) -> ("something" "chases" "cat" "+"))
If something likes the cow then it needs the cat.
((("something" "likes" "cow" "+")) -> ("something" "needs" "cat" "+"))
If the lion likes the cat and the cat needs the cow then the cow is cold.
((("lion" "likes" "cat" "+") ("cat" "needs" "cow" "+")) -> ("cow" "is" "cold" "+"))
The lion likes the cow.
True
1
proof
[(triple3)]
("lion" "likes" "cow" "+")
triple3
The lion does not like the cow.
False
1
inv-proof
[(triple3)]
("lion" "likes" "cow" "-")
triple3
The lion needs the cat.
True
2
proof
[(((triple3) -> rule7))]
("lion" "needs" "cat" "+")
((triple3) -> (rule7 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The lion does not need the cow.
False
3
inv-proof
[(((triple2 triple3) -> rule4))]
("lion" "needs" "cow" "-")
((triple2 triple3) -> (rule4 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion chases the lion.
True
3
proof
[(((((triple3) -> rule7)) -> rule3))]
("lion" "chases" "lion" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The lion does not chase the lion.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3))]
("lion" "chases" "lion" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "chases" "cat" "-")
The cow needs the cat.
Unknown
rconc
[@1: The cow needs the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "needs" "cat" "+")
The lion does not chase the cat.
Unknown
inv-rconc
[@2: The lion chases the cat.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("lion" "chases" "cat" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The cat does not like the cow.
Unknown
inv-random
[@0: The cat likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cow" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat is blue.[(triple1)] The cow likes the lion.[(triple2)] The lion likes the cow.[(triple3)] @1: The lion needs the cat.[(((triple3) -> rule7))] The lion needs the cow.[(((triple2 triple3) -> rule4))] @2: The lion chases the lion.[(((((triple3) -> rule7)) -> rule3))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cow likes the lion.
("cow" "likes" "lion" "+")
triple2
The lion likes the cow.
("lion" "likes" "cow" "+")
triple3
The lion needs the cat.
("lion" "needs" "cat" "+")
((triple3) -> (rule7 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
((triple2 triple3) -> (rule4 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2