The cat eats the lion. The cat is not nice. The cat does not like the lion. The cat sees the lion. The lion eats the cat. The lion does not like the cat. The lion sees the cat. If something is cold then it likes the lion. If something is blue and not nice then it does not eat the lion. If something is blue and it sees the cat then it is not young. If something likes the cat then it does not see the cat. If something likes the lion then the lion sees the cat. If the cat sees the lion then the cat is young. If something is nice and not young then it eats the cat. If the lion eats the cat then the lion is kind.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat does not like the lion.
("cat" "likes" "lion" "-")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion does not like the cat.
("lion" "likes" "cat" "-")
The lion sees the cat.
("lion" "sees" "cat" "+")
If something is cold then it likes the lion.
((("something" "is" "cold" "+")) -> ("something" "likes" "lion" "+"))
If something is blue and not nice then it does not eat the lion.
((("something" "is" "blue" "+") ("something" "is" "nice" "~")) -> ("something" "eats" "lion" "-"))
If something is blue and it sees the cat then it is not young.
((("something" "is" "blue" "+") ("something" "sees" "cat" "+")) -> ("something" "is" "young" "-"))
If something likes the cat then it does not see the cat.
((("something" "likes" "cat" "+")) -> ("something" "sees" "cat" "-"))
If something likes the lion then the lion sees the cat.
((("something" "likes" "lion" "+")) -> ("lion" "sees" "cat" "+"))
If the cat sees the lion then the cat is young.
((("cat" "sees" "lion" "+")) -> ("cat" "is" "young" "+"))
If something is nice and not young then it eats the cat.
((("something" "is" "nice" "+") ("something" "is" "young" "~")) -> ("something" "eats" "cat" "+"))
If the lion eats the cat then the lion is kind.
((("lion" "eats" "cat" "+")) -> ("lion" "is" "kind" "+"))
The cat does not like the lion.
True
1
proof
[(triple3)]
("cat" "likes" "lion" "-")
triple3
The cat likes the lion.
False
1
inv-proof
[(triple3)]
("cat" "likes" "lion" "+")
triple3
The lion is kind.
True
2
proof
[(((triple5) -> rule8))]
("lion" "is" "kind" "+")
((triple5) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The cat is not young.
False
2
inv-proof
[(((triple4) -> rule6))]
("cat" "is" "young" "-")
((triple4) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "eats" "cat" "-")
The lion likes the lion.
Unknown
rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "lion" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The cat does not like the lion.[(triple3)] The cat eats the lion.[(triple1)] The cat is not nice.[(triple2)] The cat sees the lion.[(triple4)] The lion does not like the cat.[(triple6)] The lion eats the cat.[(triple5)] The lion sees the cat.[(triple7)] @1: The cat is young.[(((triple4) -> rule6))] The lion is kind.[(((triple5) -> rule8))]
The cat does not like the lion.
("cat" "likes" "lion" "-")
triple3
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is not nice.
("cat" "is" "nice" "-")
triple2
The cat sees the lion.
("cat" "sees" "lion" "+")
triple4
The lion does not like the cat.
("lion" "likes" "cat" "-")
triple6
The lion eats the cat.
("lion" "eats" "cat" "+")
triple5
The lion sees the cat.
("lion" "sees" "cat" "+")
triple7
The cat is young.
("cat" "is" "young" "+")
((triple4) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple5) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1