The cat is cold. The cat visits the lion. The lion likes the cat. If someone needs the cat then they are green. If someone is red then they are not green. If someone is cold then they are red.
The cat is cold.
("cat" "is" "cold" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
If someone needs the cat then they are green.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "green" "+"))
If someone is red then they are not green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "-"))
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
The cat is cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "+")
triple1
The lion does not like the cat.
False
1
inv-proof
[(triple3)]
("lion" "likes" "cat" "-")
triple3
The cat is red.
True
2
proof
[(((triple1) -> rule3))]
("cat" "is" "red" "+")
((triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "is" "red" "-")
((triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not green.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("cat" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("cat" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "red" "-")
The lion is green.
Unknown
rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "green" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The cat is cold.[(triple1)] The cat visits the lion.[(triple2)] The lion likes the cat.[(triple3)] @1: The cat is red.[(((triple1) -> rule3))] @2: The cat is not green.[(((((triple1) -> rule3)) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat visits the lion.
("cat" "visits" "lion" "+")
triple2
The lion likes the cat.
("lion" "likes" "cat" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
((triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not green.
("cat" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The cat is red.
("cat" "is" "red" "+")
int2