The cat sees the lion. The lion is round. If something visits the lion and it is not big then the lion is not kind. If the lion visits the cat then the lion does not like the cat. If something is big then it likes the cat. If the cat sees the lion then the cat visits the lion. If the lion sees the cat then the cat does not visit the lion. If the cat likes the lion and the cat visits the lion then the lion does not visit the cat. If something sees the lion and it visits the lion then it likes the lion. If something sees the lion and the lion visits the cat then the lion is round.
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion is round.
("lion" "is" "round" "+")
If something visits the lion and it is not big then the lion is not kind.
((("something" "visits" "lion" "+") ("something" "is" "big" "~")) -> ("lion" "is" "kind" "-"))
If the lion visits the cat then the lion does not like the cat.
((("lion" "visits" "cat" "+")) -> ("lion" "likes" "cat" "-"))
If something is big then it likes the cat.
((("something" "is" "big" "+")) -> ("something" "likes" "cat" "+"))
If the cat sees the lion then the cat visits the lion.
((("cat" "sees" "lion" "+")) -> ("cat" "visits" "lion" "+"))
If the lion sees the cat then the cat does not visit the lion.
((("lion" "sees" "cat" "+")) -> ("cat" "visits" "lion" "-"))
If the cat likes the lion and the cat visits the lion then the lion does not visit the cat.
((("cat" "likes" "lion" "+") ("cat" "visits" "lion" "+")) -> ("lion" "visits" "cat" "-"))
If something sees the lion and it visits the lion then it likes the lion.
((("something" "sees" "lion" "+") ("something" "visits" "lion" "+")) -> ("something" "likes" "lion" "+"))
If something sees the lion and the lion visits the cat then the lion is round.
((("something" "sees" "lion" "+") ("lion" "visits" "cat" "+")) -> ("lion" "is" "round" "+"))
The cat sees the lion.
True
1
proof
[(triple1)]
("cat" "sees" "lion" "+")
triple1
The cat does not see the lion.
False
1
inv-proof
[(triple1)]
("cat" "sees" "lion" "-")
triple1
The cat visits the lion.
True
2
proof
[(((triple1) -> rule4))]
("cat" "visits" "lion" "+")
((triple1) -> (rule4 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat does not visit the lion.
False
2
inv-proof
[(((triple1) -> rule4))]
("cat" "visits" "lion" "-")
((triple1) -> (rule4 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat likes the lion.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule7))]
("cat" "likes" "lion" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat does not like the lion.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule7))]
("cat" "likes" "lion" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "cat" "-")
The lion likes the cat.
Unknown
rconc
[@1: The lion likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "likes" "cat" "+")
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "likes" "lion" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The lion does not see the cat.
Unknown
inv-random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "-")
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 sees the lion.[(triple1)] The lion is round.[(triple2)] @1: The cat visits the lion.[(((triple1) -> rule4))] @2: The cat likes the lion.[(((triple1 ((triple1) -> rule4)) -> rule7))] @3: The lion does not visit the cat.[(((((triple1 ((triple1) -> rule4)) -> rule7) ((triple1) -> rule4)) -> rule6))]
The cat sees the lion.
("cat" "sees" "lion" "+")
triple1
The lion is round.
("lion" "is" "round" "+")
triple2
The cat visits the lion.
("cat" "visits" "lion" "+")
((triple1) -> (rule4 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The lion does not visit the cat.
("lion" "visits" "cat" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
The lion does not visit the cat.
("lion" "visits" "cat" "-")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3