The cat is cold. The cat is rough. The cat likes the lion. The cat needs the lion. The lion eats the cat. The lion is green. The lion is not kind. The lion is not rough. The lion likes the cat. The lion needs the cat. If something needs the lion then it eats the lion. If the cat eats the lion and the lion needs the cat then the cat is green.
The cat is cold.
("cat" "is" "cold" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is not rough.
("lion" "is" "rough" "-")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If something needs the lion then it eats the lion.
((("something" "needs" "lion" "+")) -> ("something" "eats" "lion" "+"))
If the cat eats the lion and the lion needs the cat then the cat is green.
((("cat" "eats" "lion" "+") ("lion" "needs" "cat" "+")) -> ("cat" "is" "green" "+"))
The lion eats the cat.
True
1
proof
[(triple5)]
("lion" "eats" "cat" "+")
triple5
The cat is not cold.
False
1
inv-proof
[(triple1)]
("cat" "is" "cold" "-")
triple1
The cat eats the lion.
True
2
proof
[(((triple4) -> rule1))]
("cat" "eats" "lion" "+")
((triple4) -> (rule1 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat does not eat the lion.
False
2
inv-proof
[(((triple4) -> rule1))]
("cat" "eats" "lion" "-")
((triple4) -> (rule1 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat is green.
True
4
proof
[(((((triple4) -> rule1) triple10) -> rule2))]
("cat" "is" "green" "+")
((((triple4) -> (rule1 % int2)) triple10) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The cat is not green.
False
4
inv-proof
[(((((triple4) -> rule1) triple10) -> rule2))]
("cat" "is" "green" "-")
((((triple4) -> (rule1 % int2)) triple10) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "lion" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat is cold.[(triple1)] The cat is rough.[(triple2)] The cat likes the lion.[(triple3)] The cat needs the lion.[(triple4)] The lion eats the cat.[(triple5)] The lion is green.[(triple6)] The lion is not kind.[(triple7)] The lion is not rough.[(triple8)] The lion likes the cat.[(triple9)] The lion needs the cat.[(triple10)] @1: The cat eats the lion.[(((triple4) -> rule1))] @2: The cat is green.[(((((triple4) -> rule1) triple10) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
The cat needs the lion.
("cat" "needs" "lion" "+")
triple4
The lion eats the cat.
("lion" "eats" "cat" "+")
triple5
The lion is green.
("lion" "is" "green" "+")
triple6
The lion is not kind.
("lion" "is" "kind" "-")
triple7
The lion is not rough.
("lion" "is" "rough" "-")
triple8
The lion likes the cat.
("lion" "likes" "cat" "+")
triple9
The lion needs the cat.
("lion" "needs" "cat" "+")
triple10
The cat eats the lion.
("cat" "eats" "lion" "+")
((triple4) -> (rule1 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat is green.
("cat" "is" "green" "+")
((((triple4) -> (rule1 % int2)) triple10) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2