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