The bald eagle chases the cat. The cat is young. The dog is not red. The rabbit visits the bald eagle. If the dog chases the rabbit and the dog does not visit the bald eagle then the dog needs the bald eagle. If someone chases the cat then the cat needs the bald eagle. If someone chases the cat then the cat visits the rabbit. If the bald eagle chases the cat and the bald eagle is not young then the bald eagle needs the rabbit. If someone is red and big then they visit the dog. If someone needs the bald eagle then they are round. If someone is young and round then they need the cat. If the cat is blue and the cat does not visit the rabbit then the cat visits the dog.
The bald eagle chases the cat.
("bald eagle" "chases" "cat" "+")
The cat is young.
("cat" "is" "young" "+")
The dog is not red.
("dog" "is" "red" "-")
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
If the dog chases the rabbit and the dog does not visit the bald eagle then the dog needs the bald eagle.
((("dog" "chases" "rabbit" "+") ("dog" "visits" "bald eagle" "~")) -> ("dog" "needs" "bald eagle" "+"))
If someone chases the cat then the cat needs the bald eagle.
((("someone" "chases" "cat" "+")) -> ("cat" "needs" "bald eagle" "+"))
If someone chases the cat then the cat visits the rabbit.
((("someone" "chases" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If the bald eagle chases the cat and the bald eagle is not young then the bald eagle needs the rabbit.
((("bald eagle" "chases" "cat" "+") ("bald eagle" "is" "young" "~")) -> ("bald eagle" "needs" "rabbit" "+"))
If someone is red and big then they visit the dog.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "visits" "dog" "+"))
If someone needs the bald eagle then they are round.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "is" "round" "+"))
If someone is young and round then they need the cat.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "needs" "cat" "+"))
If the cat is blue and the cat does not visit the rabbit then the cat visits the dog.
((("cat" "is" "blue" "+") ("cat" "visits" "rabbit" "~")) -> ("cat" "visits" "dog" "+"))
The dog is not red.
True
1
proof
[(triple3)]
("dog" "is" "red" "-")
triple3
The cat is not young.
False
1
inv-proof
[(triple2)]
("cat" "is" "young" "-")
triple2
The cat needs the bald eagle.
True
2
proof
[(((triple1) -> rule2))]
("cat" "needs" "bald eagle" "+")
((triple1) -> (rule2 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The cat does not visit the rabbit.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "visits" "rabbit" "-")
((triple1) -> (rule3 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is round.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("cat" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int2
The cat is not round.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("cat" "is" "round" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int2
The cat needs the cat.
True
5
proof
[(((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule7))]
("cat" "needs" "cat" "+")
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int3
The cat does not need the cat.
False
5
inv-proof
[(((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule7))]
("cat" "needs" "cat" "-")
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int3
The dog does not need the cat.
Unknown
inv-rconc
[@1: The dog needs the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "needs" "cat" "-")
The bald eagle is round.
Unknown
rconc
[@1: The bald eagle is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "round" "+")
The rabbit does not need the cat.
Unknown
inv-rconc
[@1: The rabbit needs the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "needs" "cat" "-")
The dog is round.
Unknown
rconc
[@2: The dog is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("dog" "is" "round" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The bald eagle visits the bald eagle.
Unknown
random
[@0: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "bald eagle" "+")
The cat does not need the rabbit.
Unknown
inv-random
[@0: The cat needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "rabbit" "-")
The dog chases the rabbit.
Unknown
random
[@0: The dog chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "rabbit" "+")
@0: The bald eagle chases the cat.[(triple1)] The cat is young.[(triple2)] The dog is not red.[(triple3)] The rabbit visits the bald eagle.[(triple4)] @1: The cat needs the bald eagle.[(((triple1) -> rule2))] The cat visits the rabbit.[(((triple1) -> rule3))] @2: The cat is round.[(((((triple1) -> rule2)) -> rule6))] @3: The cat needs the cat.[(((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule7))]
The bald eagle chases the cat.
("bald eagle" "chases" "cat" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The dog is not red.
("dog" "is" "red" "-")
triple3
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
triple4
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
((triple1) -> (rule2 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((triple1) -> (rule3 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int3