The cat does not chase the dog. The cat chases the rabbit. The cat does not need the dog. The cat needs the lion. The dog does not chase the cat. The dog chases the rabbit. The dog is kind. The dog sees the rabbit. The lion sees the cat. The rabbit is red. If someone sees the cat then the cat is red. If someone is red then they do not see the dog. If someone sees the lion then the lion does not need the rabbit. If someone is red and they do not see the cat then they chase the rabbit. If someone is kind then they do not need the lion. If someone is young and they see the cat then they chase the dog.
The cat does not chase the dog.
("cat" "chases" "dog" "-")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat does not need the dog.
("cat" "needs" "dog" "-")
The cat needs the lion.
("cat" "needs" "lion" "+")
The dog does not chase the cat.
("dog" "chases" "cat" "-")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
If someone sees the cat then the cat is red.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone is red then they do not see the dog.
((("someone" "is" "red" "+")) -> ("someone" "sees" "dog" "-"))
If someone sees the lion then the lion does not need the rabbit.
((("someone" "sees" "lion" "+")) -> ("lion" "needs" "rabbit" "-"))
If someone is red and they do not see the cat then they chase the rabbit.
((("someone" "is" "red" "+") ("someone" "sees" "cat" "~")) -> ("someone" "chases" "rabbit" "+"))
If someone is kind then they do not need the lion.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "lion" "-"))
If someone is young and they see the cat then they chase the dog.
((("someone" "is" "young" "+") ("someone" "sees" "cat" "+")) -> ("someone" "chases" "dog" "+"))
The cat does not chase the dog.
True
1
proof
[(triple1)]
("cat" "chases" "dog" "-")
triple1
The dog does not see the rabbit.
False
1
inv-proof
[(triple8)]
("dog" "sees" "rabbit" "-")
triple8
The rabbit does not see the dog.
True
2
proof
[(((triple10) -> rule2))]
("rabbit" "sees" "dog" "-")
((triple10) -> (rule2 % int1))
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
int1
The rabbit sees the dog.
False
2
inv-proof
[(((triple10) -> rule2))]
("rabbit" "sees" "dog" "+")
((triple10) -> (rule2 % int1))
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
int1
The cat does not see the dog.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("cat" "sees" "dog" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The cat does not see the dog.
("cat" "sees" "dog" "-")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat sees the dog.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule2))]
("cat" "sees" "dog" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The cat does not see the dog.
("cat" "sees" "dog" "-")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The rabbit does not chase the dog.
Unknown
inv-rconc
[@1: The rabbit chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "chases" "dog" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The lion does not chase the rabbit.
Unknown
inv-rconc
[@1: The lion chases the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "chases" "rabbit" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The dog does not chase the lion.
Unknown
inv-random
[@0: The dog chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "lion" "-")
The dog sees the lion.
Unknown
random
[@0: The dog sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "lion" "+")
@0: The cat chases the rabbit.[(triple2)] The cat does not chase the dog.[(triple1)] The cat does not need the dog.[(triple3)] The cat needs the lion.[(triple4)] The dog chases the rabbit.[(triple6)] The dog does not chase the cat.[(triple5)] The dog is kind.[(triple7)] The dog sees the rabbit.[(triple8)] The lion sees the cat.[(triple9)] The rabbit is red.[(triple10)] @1: The cat is red.[(((triple9) -> rule1))] The dog does not need the lion.[(((triple7) -> rule5))] The rabbit does not see the dog.[(((triple10) -> rule2))] @2: The cat does not see the dog.[(((((triple9) -> rule1)) -> rule2))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The cat does not chase the dog.
("cat" "chases" "dog" "-")
triple1
The cat does not need the dog.
("cat" "needs" "dog" "-")
triple3
The cat needs the lion.
("cat" "needs" "lion" "+")
triple4
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple6
The dog does not chase the cat.
("dog" "chases" "cat" "-")
triple5
The dog is kind.
("dog" "is" "kind" "+")
triple7
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple8
The lion sees the cat.
("lion" "sees" "cat" "+")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple10
The cat is red.
("cat" "is" "red" "+")
((triple9) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The dog does not need the lion.
("dog" "needs" "lion" "-")
((triple7) -> (rule5 % int1))
The dog does not need the lion.
("dog" "needs" "lion" "-")
int1
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
((triple10) -> (rule2 % int1))
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
int1
The cat does not see the dog.
("cat" "sees" "dog" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The cat does not see the dog.
("cat" "sees" "dog" "-")
int1
The cat is red.
("cat" "is" "red" "+")
int2