The cat eats the lion. The cat is kind. The lion is cold. If something visits the lion and it sees the lion then it is cold. If something eats the cat and it is cold then it sees the lion. If something visits the cat and the cat eats the lion then the lion is red. If something eats the cat then it visits the lion. If something eats the lion and it is blue then the lion visits the cat. If something visits the cat and the cat eats the lion then it visits the lion. If something visits the lion and it is red then the lion is red. If something eats the lion then the lion visits the cat.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is kind.
("cat" "is" "kind" "+")
The lion is cold.
("lion" "is" "cold" "+")
If something visits the lion and it sees the lion then it is cold.
((("something" "visits" "lion" "+") ("something" "sees" "lion" "+")) -> ("something" "is" "cold" "+"))
If something eats the cat and it is cold then it sees the lion.
((("something" "eats" "cat" "+") ("something" "is" "cold" "+")) -> ("something" "sees" "lion" "+"))
If something visits the cat and the cat eats the lion then the lion is red.
((("something" "visits" "cat" "+") ("cat" "eats" "lion" "+")) -> ("lion" "is" "red" "+"))
If something eats the cat then it visits the lion.
((("something" "eats" "cat" "+")) -> ("something" "visits" "lion" "+"))
If something eats the lion and it is blue then the lion visits the cat.
((("something" "eats" "lion" "+") ("something" "is" "blue" "+")) -> ("lion" "visits" "cat" "+"))
If something visits the cat and the cat eats the lion then it visits the lion.
((("something" "visits" "cat" "+") ("cat" "eats" "lion" "+")) -> ("something" "visits" "lion" "+"))
If something visits the lion and it is red then the lion is red.
((("something" "visits" "lion" "+") ("something" "is" "red" "+")) -> ("lion" "is" "red" "+"))
If something eats the lion then the lion visits the cat.
((("something" "eats" "lion" "+")) -> ("lion" "visits" "cat" "+"))
The cat is kind.
True
1
proof
[(triple2)]
("cat" "is" "kind" "+")
triple2
The cat does not eat the lion.
False
1
inv-proof
[(triple1)]
("cat" "eats" "lion" "-")
triple1
The lion visits the cat.
True
2
proof
[(((triple1) -> rule8))]
("lion" "visits" "cat" "+")
((triple1) -> (rule8 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion does not visit the cat.
False
2
inv-proof
[(((triple1) -> rule8))]
("lion" "visits" "cat" "-")
((triple1) -> (rule8 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion visits the lion.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule6))]
("lion" "visits" "lion" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion is not red.
False
4
inv-proof
[(((((triple1) -> rule8) triple1) -> rule3))]
("lion" "is" "red" "-")
((((triple1) -> (rule8 % int2)) triple1) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat does not visit the lion.
Unknown
inv-rconc
[@1: The cat visits the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "lion" "-")
The cat is cold.
Unknown
rconc
[@2: The cat is cold.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("cat" "is" "cold" "+")
The cat does not see the lion.
Unknown
inv-rconc
[@1: The cat sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "lion" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat eats the lion.[(triple1)] The cat is kind.[(triple2)] The lion is cold.[(triple3)] @1: The lion visits the cat.[(((triple1) -> rule8))] @2: The lion is red.[(((((triple1) -> rule8) triple1) -> rule3))] The lion visits the lion.[(((((triple1) -> rule8) triple1) -> rule6))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple1) -> (rule8 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2