The cat chases the dog. The cat is big. The cat needs the dog. The cat visits the rabbit. The dog is big. The dog is cold. The dog is round. The dog needs the cat. The dog needs the rabbit. The dog visits the rabbit. The rabbit chases the cat. The rabbit needs the dog. If someone is big then they need the cat. If the cat chases the rabbit then the rabbit chases the dog. If someone needs the cat and they need the dog then they chase the rabbit. Blue, green people are round. If someone needs the dog and the dog is big then they are cold. If someone chases the cat then they are green.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is big.
("cat" "is" "big" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
If someone is big then they need the cat.
((("someone" "is" "big" "+")) -> ("someone" "needs" "cat" "+"))
If the cat chases the rabbit then the rabbit chases the dog.
((("cat" "chases" "rabbit" "+")) -> ("rabbit" "chases" "dog" "+"))
If someone needs the cat and they need the dog then they chase the rabbit.
((("someone" "needs" "cat" "+") ("someone" "needs" "dog" "+")) -> ("someone" "chases" "rabbit" "+"))
Blue, green people are round.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone needs the dog and the dog is big then they are cold.
((("someone" "needs" "dog" "+") ("dog" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone chases the cat then they are green.
((("someone" "chases" "cat" "+")) -> ("someone" "is" "green" "+"))
The rabbit needs the dog.
True
1
proof
[(triple12)]
("rabbit" "needs" "dog" "+")
triple12
The cat does not chase the dog.
False
1
inv-proof
[(triple1)]
("cat" "chases" "dog" "-")
triple1
The cat needs the cat.
True
2
proof
[(((triple2) -> rule1))]
("cat" "needs" "cat" "+")
((triple2) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The rabbit is not cold.
False
3
inv-proof
[(((triple12 triple5) -> rule5))]
("rabbit" "is" "cold" "-")
((triple12 triple5) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cat chases the rabbit.
True
4
proof
[(((((triple2) -> rule1) triple3) -> rule3))]
("cat" "chases" "rabbit" "+")
((((triple2) -> (rule1 % int2)) triple3) -> (rule3 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat does not chase the rabbit.
False
4
inv-proof
[(((((triple2) -> rule1) triple3) -> rule3))]
("cat" "chases" "rabbit" "-")
((((triple2) -> (rule1 % int2)) triple3) -> (rule3 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The rabbit chases the dog.
True
5
proof
[(((((((triple2) -> rule1) triple3) -> rule3)) -> rule2))]
("rabbit" "chases" "dog" "+")
((((((triple2) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The rabbit does not chase the dog.
False
5
inv-proof
[(((((((triple2) -> rule1) triple3) -> rule3)) -> rule2))]
("rabbit" "chases" "dog" "-")
((((((triple2) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "round" "-")
The dog chases the rabbit.
Unknown
rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "rabbit" "+")
The rabbit does not need the cat.
Unknown
inv-rconc
[@1: The rabbit needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "cat" "-")
The rabbit is round.
Unknown
rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "round" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The cat chases the dog.[(triple1)] The cat is big.[(triple2)] The cat needs the dog.[(triple3)] The cat visits the rabbit.[(triple4)] The dog is big.[(triple5)] The dog is cold.[(triple6)] The dog is round.[(triple7)] The dog needs the cat.[(triple8 OR ((triple5) -> rule1))] The dog needs the rabbit.[(triple9)] The dog visits the rabbit.[(triple10)] The rabbit chases the cat.[(triple11)] The rabbit needs the dog.[(triple12)] @1: The cat is cold.[(((triple3 triple5) -> rule5))] The cat needs the cat.[(((triple2) -> rule1))] The rabbit is cold.[(((triple12 triple5) -> rule5))] The rabbit is green.[(((triple11) -> rule6))] @2: The cat chases the rabbit.[(((((triple2) -> rule1) triple3) -> rule3))] @3: The rabbit chases the dog.[(((((((triple2) -> rule1) triple3) -> rule3)) -> rule2))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat needs the dog.
("cat" "needs" "dog" "+")
triple3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog is cold.
("dog" "is" "cold" "+")
triple6
The dog is round.
("dog" "is" "round" "+")
triple7
The dog needs the cat.
("dog" "needs" "cat" "+")
triple8
((triple5) -> (rule1 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple9
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple10
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple11
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple12
The cat is cold.
("cat" "is" "cold" "+")
((triple3 triple5) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple2) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple12 triple5) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple11) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((((triple2) -> (rule1 % int2)) triple3) -> (rule3 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((((((triple2) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3