The cat chases the lion. The cat is not big. The cat is red. The cat needs the dog. The cat needs the lion. The cat visits the dog. The dog is kind. The dog is red. The dog needs the cat. The dog visits the lion. The lion chases the dog. The lion is not kind. The lion needs the cat. The lion needs the dog. The lion visits the cat. If someone is big then they chase the dog. If someone is round then they chase the dog. If the lion chases the cat and the lion is not red then the cat chases the dog. If someone visits the lion and they need the cat then the cat is round. If someone chases the lion then the lion is round. If someone is round and they chase the cat then the cat visits the dog. If someone chases the lion then the lion chases the cat. If someone visits the dog and the dog chases the cat then the dog chases the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is not big.
("cat" "is" "big" "-")
The cat is red.
("cat" "is" "red" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone is big then they chase the dog.
((("someone" "is" "big" "+")) -> ("someone" "chases" "dog" "+"))
If someone is round then they chase the dog.
((("someone" "is" "round" "+")) -> ("someone" "chases" "dog" "+"))
If the lion chases the cat and the lion is not red then the cat chases the dog.
((("lion" "chases" "cat" "+") ("lion" "is" "red" "~")) -> ("cat" "chases" "dog" "+"))
If someone visits the lion and they need the cat then the cat is round.
((("someone" "visits" "lion" "+") ("someone" "needs" "cat" "+")) -> ("cat" "is" "round" "+"))
If someone chases the lion then the lion is round.
((("someone" "chases" "lion" "+")) -> ("lion" "is" "round" "+"))
If someone is round and they chase the cat then the cat visits the dog.
((("someone" "is" "round" "+") ("someone" "chases" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If someone chases the lion then the lion chases the cat.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "cat" "+"))
If someone visits the dog and the dog chases the cat then the dog chases the lion.
((("someone" "visits" "dog" "+") ("dog" "chases" "cat" "+")) -> ("dog" "chases" "lion" "+"))
The lion needs the cat.
True
1
proof
[(triple13)]
("lion" "needs" "cat" "+")
triple13
The lion does not chase the dog.
False
1
inv-proof
[(triple11 OR ((((triple1) -> rule5)) -> rule2))]
("lion" "chases" "dog" "-")
triple11
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is round.
True
2
proof
[(((triple1) -> rule5))]
("lion" "is" "round" "+")
((triple1) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion does not chase the cat.
False
2
inv-proof
[(((triple1) -> rule7))]
("lion" "chases" "cat" "-")
((triple1) -> (rule7 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The dog does not chase the lion.
Unknown
inv-rconc
[@1: The dog chases the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "chases" "lion" "-")
The dog chases the dog.
Unknown
rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "dog" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The cat chases the lion.[(triple1)] The cat is not big.[(triple2)] The cat is red.[(triple3)] The cat needs the dog.[(triple4)] The cat needs the lion.[(triple5)] The cat visits the dog.[(triple6 OR ((((triple1) -> rule5) ((triple1) -> rule7)) -> rule6))] The dog is kind.[(triple7)] The dog is red.[(triple8)] The dog needs the cat.[(triple9)] The dog visits the lion.[(triple10)] The lion chases the dog.[(triple11 OR ((((triple1) -> rule5)) -> rule2))] The lion is not kind.[(triple12)] The lion needs the cat.[(triple13)] The lion needs the dog.[(triple14)] The lion visits the cat.[(triple15)] @1: The cat is round.[(((triple10 triple9) -> rule4))] The lion chases the cat.[(((triple1) -> rule7))] The lion is round.[(((triple1) -> rule5))] @2: The cat chases the dog.[(((((triple10 triple9) -> rule4)) -> rule2))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat is not big.
("cat" "is" "big" "-")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat needs the dog.
("cat" "needs" "dog" "+")
triple4
The cat needs the lion.
("cat" "needs" "lion" "+")
triple5
The cat visits the dog.
("cat" "visits" "dog" "+")
triple6
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
triple7
The dog is red.
("dog" "is" "red" "+")
triple8
The dog needs the cat.
("dog" "needs" "cat" "+")
triple9
The dog visits the lion.
("dog" "visits" "lion" "+")
triple10
The lion chases the dog.
("lion" "chases" "dog" "+")
triple11
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is not kind.
("lion" "is" "kind" "-")
triple12
The lion needs the cat.
("lion" "needs" "cat" "+")
triple13
The lion needs the dog.
("lion" "needs" "dog" "+")
triple14
The lion visits the cat.
("lion" "visits" "cat" "+")
triple15
The cat is round.
("cat" "is" "round" "+")
((triple10 triple9) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
((triple1) -> (rule7 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((triple1) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
((((triple10 triple9) -> (rule4 % int2))) -> (rule2 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2