The bald eagle is rough. The bald eagle needs the cat. The bald eagle needs the dog. The bald eagle visits the cat. The cat chases the bald eagle. The cat chases the dog. The cat visits the bald eagle. The dog visits the cat. The tiger is rough. The tiger needs the cat. The tiger needs the dog. The tiger visits the cat. If someone is nice and they need the cat then the cat chases the bald eagle. If someone needs the tiger then the tiger visits the bald eagle. If someone visits the cat then the cat needs the tiger. If the dog is green and the dog is kind then the dog is nice. If someone is nice and they need the cat then the cat visits the dog. If someone visits the bald eagle and the bald eagle visits the tiger then they are rough. If someone needs the cat then the cat is nice. If the dog needs the tiger and the dog is round then the tiger needs the bald eagle.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
The cat chases the bald eagle.
("cat" "chases" "bald eagle" "+")
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone is nice and they need the cat then the cat chases the bald eagle.
((("someone" "is" "nice" "+") ("someone" "needs" "cat" "+")) -> ("cat" "chases" "bald eagle" "+"))
If someone needs the tiger then the tiger visits the bald eagle.
((("someone" "needs" "tiger" "+")) -> ("tiger" "visits" "bald eagle" "+"))
If someone visits the cat then the cat needs the tiger.
((("someone" "visits" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
If the dog is green and the dog is kind then the dog is nice.
((("dog" "is" "green" "+") ("dog" "is" "kind" "+")) -> ("dog" "is" "nice" "+"))
If someone is nice and they need the cat then the cat visits the dog.
((("someone" "is" "nice" "+") ("someone" "needs" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If someone visits the bald eagle and the bald eagle visits the tiger then they are rough.
((("someone" "visits" "bald eagle" "+") ("bald eagle" "visits" "tiger" "+")) -> ("someone" "is" "rough" "+"))
If someone needs the cat then the cat is nice.
((("someone" "needs" "cat" "+")) -> ("cat" "is" "nice" "+"))
If the dog needs the tiger and the dog is round then the tiger needs the bald eagle.
((("dog" "needs" "tiger" "+") ("dog" "is" "round" "+")) -> ("tiger" "needs" "bald eagle" "+"))
The tiger is rough.
True
1
proof
[(triple9)]
("tiger" "is" "rough" "+")
triple9
The bald eagle does not need the dog.
False
1
inv-proof
[(triple3)]
("bald eagle" "needs" "dog" "-")
triple3
The cat needs the tiger.
True
2
proof
[(((triple12) -> rule3) OR ((triple4) -> rule3) OR ((triple8) -> rule3))]
("cat" "needs" "tiger" "+")
((triple12) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((triple4) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((triple8) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat does not need the tiger.
False
2
inv-proof
[(((triple12) -> rule3) OR ((triple4) -> rule3) OR ((triple8) -> rule3))]
("cat" "needs" "tiger" "-")
((triple12) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((triple4) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((triple8) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger visits the bald eagle.
True
3
proof
[(((((triple12) -> rule3)) -> rule2) OR ((((triple4) -> rule3)) -> rule2) OR ((((triple8) -> rule3)) -> rule2))]
("tiger" "visits" "bald eagle" "+")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger does not visit the bald eagle.
False
3
inv-proof
[(((((triple12) -> rule3)) -> rule2) OR ((((triple4) -> rule3)) -> rule2) OR ((((triple8) -> rule3)) -> rule2))]
("tiger" "visits" "bald eagle" "-")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "nice" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "rough" "+")
The tiger does not need the bald eagle.
Unknown
inv-rconc
[@1: The tiger needs the bald eagle.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "needs" "bald eagle" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The dog chases the tiger.
Unknown
random
[@0: The dog chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "tiger" "+")
@0: The bald eagle is rough.[(triple1)] The bald eagle needs the cat.[(triple2)] The bald eagle needs the dog.[(triple3)] The bald eagle visits the cat.[(triple4)] The cat chases the bald eagle.[(triple5)] The cat chases the dog.[(triple6)] The cat visits the bald eagle.[(triple7)] The dog visits the cat.[(triple8)] The tiger is rough.[(triple9)] The tiger needs the cat.[(triple10)] The tiger needs the dog.[(triple11)] The tiger visits the cat.[(triple12)] @1: The cat is nice.[(((triple10) -> rule7) OR ((triple2) -> rule7))] The cat needs the tiger.[(((triple12) -> rule3) OR ((triple4) -> rule3) OR ((triple8) -> rule3))] @2: The tiger visits the bald eagle.[(((((triple12) -> rule3)) -> rule2) OR ((((triple4) -> rule3)) -> rule2) OR ((((triple8) -> rule3)) -> rule2))]
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
triple2
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple3
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
triple4
The cat chases the bald eagle.
("cat" "chases" "bald eagle" "+")
triple5
The cat chases the dog.
("cat" "chases" "dog" "+")
triple6
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
triple7
The dog visits the cat.
("dog" "visits" "cat" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple10
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple11
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple12
The cat is nice.
("cat" "is" "nice" "+")
((triple10) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((triple2) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((triple12) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((triple4) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((triple8) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2