The cat is big. The cat sees the lion. The lion is big. The lion is green. The lion is kind. The lion is red. The lion is round. The lion likes the cat. The lion sees the cat. The lion visits the cat. If something visits the cat then it likes the lion. If something likes the lion then the lion likes the cat. If something sees the cat and the cat is red then the cat is green. If something likes the cat and the cat is big then the cat visits the lion. If something is round and it likes the cat then the cat sees the lion. If something is green and red then it visits the lion.
The cat is big.
("cat" "is" "big" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If something visits the cat then it likes the lion.
((("something" "visits" "cat" "+")) -> ("something" "likes" "lion" "+"))
If something likes the lion then the lion likes the cat.
((("something" "likes" "lion" "+")) -> ("lion" "likes" "cat" "+"))
If something sees the cat and the cat is red then the cat is green.
((("something" "sees" "cat" "+") ("cat" "is" "red" "+")) -> ("cat" "is" "green" "+"))
If something likes the cat and the cat is big then the cat visits the lion.
((("something" "likes" "cat" "+") ("cat" "is" "big" "+")) -> ("cat" "visits" "lion" "+"))
If something is round and it likes the cat then the cat sees the lion.
((("something" "is" "round" "+") ("something" "likes" "cat" "+")) -> ("cat" "sees" "lion" "+"))
If something is green and red then it visits the lion.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "visits" "lion" "+"))
The lion is green.
True
1
proof
[(triple4)]
("lion" "is" "green" "+")
triple4
The lion does not see the cat.
False
1
inv-proof
[(triple9)]
("lion" "sees" "cat" "-")
triple9
The cat visits the lion.
True
3
proof
[(((triple8 triple1) -> rule4) OR ((((((triple10) -> rule1)) -> rule2) triple1) -> rule4))]
("cat" "visits" "lion" "+")
((triple8 triple1) -> (rule4 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
((((((triple10) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule4 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion does not visit the lion.
False
3
inv-proof
[(((triple4 triple6) -> rule6))]
("lion" "visits" "lion" "-")
((triple4 triple6) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "green" "-")
The cat likes the lion.
Unknown
rconc
[@1: The cat likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "lion" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat is big.[(triple1)] The cat sees the lion.[(triple2 OR ((triple7 triple8) -> rule5) OR ((triple7 ((((triple10) -> rule1)) -> rule2)) -> rule5))] The lion is big.[(triple3)] The lion is green.[(triple4)] The lion is kind.[(triple5)] The lion is red.[(triple6)] The lion is round.[(triple7)] The lion likes the cat.[(triple8 OR ((((triple10) -> rule1)) -> rule2))] The lion sees the cat.[(triple9)] The lion visits the cat.[(triple10)] @1: The cat visits the lion.[(((triple8 triple1) -> rule4) OR ((((((triple10) -> rule1)) -> rule2) triple1) -> rule4))] The lion likes the lion.[(((triple10) -> rule1))] The lion visits the lion.[(((triple4 triple6) -> rule6))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat sees the lion.
("cat" "sees" "lion" "+")
triple2
((triple7 triple8) -> (rule5 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
((triple7 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple5
The lion is red.
("lion" "is" "red" "+")
triple6
The lion is round.
("lion" "is" "round" "+")
triple7
The lion likes the cat.
("lion" "likes" "cat" "+")
triple8
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
triple9
The lion visits the cat.
("lion" "visits" "cat" "+")
triple10
The cat visits the lion.
("cat" "visits" "lion" "+")
((triple8 triple1) -> (rule4 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
((((((triple10) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule4 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple10) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple4 triple6) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1