The cat is big. The cat is cold. The cat is not rough. The cat visits the lion. The lion is cold. The lion needs the cat. The lion visits the cat. If someone is young then they see the lion. If someone needs the cat and the cat is cold then they see the lion. If someone sees the cat and the cat is red then the cat is big. If someone is red and they need the cat then they visit the cat. If someone sees the lion then the lion sees the cat. If someone is young and they need the lion then they need the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is not rough.
("cat" "is" "rough" "-")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone is young then they see the lion.
((("someone" "is" "young" "+")) -> ("someone" "sees" "lion" "+"))
If someone needs the cat and the cat is cold then they see the lion.
((("someone" "needs" "cat" "+") ("cat" "is" "cold" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the cat and the cat is red then the cat is big.
((("someone" "sees" "cat" "+") ("cat" "is" "red" "+")) -> ("cat" "is" "big" "+"))
If someone is red and they need the cat then they visit the cat.
((("someone" "is" "red" "+") ("someone" "needs" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If someone sees the lion then the lion sees the cat.
((("someone" "sees" "lion" "+")) -> ("lion" "sees" "cat" "+"))
If someone is young and they need the lion then they need the cat.
((("someone" "is" "young" "+") ("someone" "needs" "lion" "+")) -> ("someone" "needs" "cat" "+"))
The lion needs the cat.
True
1
proof
[(triple6)]
("lion" "needs" "cat" "+")
triple6
The lion does not visit the cat.
False
1
inv-proof
[(triple7)]
("lion" "visits" "cat" "-")
triple7
The lion sees the lion.
True
3
proof
[(((triple6 triple2) -> rule2))]
("lion" "sees" "lion" "+")
((triple6 triple2) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
3
inv-proof
[(((triple6 triple2) -> rule2))]
("lion" "sees" "lion" "-")
((triple6 triple2) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the cat.
True
4
proof
[(((((triple6 triple2) -> rule2)) -> rule5))]
("lion" "sees" "cat" "+")
((((triple6 triple2) -> (rule2 % int2))) -> (rule5 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion does not see the cat.
False
4
inv-proof
[(((((triple6 triple2) -> rule2)) -> rule5))]
("lion" "sees" "cat" "-")
((((triple6 triple2) -> (rule2 % int2))) -> (rule5 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "needs" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat does not see the lion.
Unknown
inv-rconc
[@2: The cat sees the lion.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("cat" "sees" "lion" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The cat is big.[(triple1)] The cat is cold.[(triple2)] The cat is not rough.[(triple3)] The cat visits the lion.[(triple4)] The lion is cold.[(triple5)] The lion needs the cat.[(triple6)] The lion visits the cat.[(triple7)] @1: The lion sees the lion.[(((triple6 triple2) -> rule2))] @2: The lion sees the cat.[(((((triple6 triple2) -> rule2)) -> rule5))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is not rough.
("cat" "is" "rough" "-")
triple3
The cat visits the lion.
("cat" "visits" "lion" "+")
triple4
The lion is cold.
("lion" "is" "cold" "+")
triple5
The lion needs the cat.
("lion" "needs" "cat" "+")
triple6
The lion visits the cat.
("lion" "visits" "cat" "+")
triple7
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple6 triple2) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
((((triple6 triple2) -> (rule2 % int2))) -> (rule5 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2