The bald eagle chases the cat. The bald eagle is not red. The bald eagle visits the tiger. The cat does not chase the tiger. The cat is rough. The cat does not like the bald eagle. The cat visits the bald eagle. The cat visits the rabbit. The rabbit chases the bald eagle. The tiger chases the cat. If something visits the tiger and the tiger is kind then the tiger visits the rabbit. If the tiger likes the bald eagle then the tiger visits the rabbit. If something likes the rabbit then it is red. If something visits the bald eagle then the bald eagle chases the tiger. If the cat is not rough and the cat does not chase the tiger then the cat is blue. If something chases the tiger then it is kind. If something is kind and it does not like the rabbit then it does not visit the rabbit. If something likes the cat and it is nice then it chases the cat.
The bald eagle chases the cat.
("bald eagle" "chases" "cat" "+")
The bald eagle is not red.
("bald eagle" "is" "red" "-")
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
The cat is rough.
("cat" "is" "rough" "+")
The cat does not like the bald eagle.
("cat" "likes" "bald eagle" "-")
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
If something visits the tiger and the tiger is kind then the tiger visits the rabbit.
((("something" "visits" "tiger" "+") ("tiger" "is" "kind" "+")) -> ("tiger" "visits" "rabbit" "+"))
If the tiger likes the bald eagle then the tiger visits the rabbit.
((("tiger" "likes" "bald eagle" "+")) -> ("tiger" "visits" "rabbit" "+"))
If something likes the rabbit then it is red.
((("something" "likes" "rabbit" "+")) -> ("something" "is" "red" "+"))
If something visits the bald eagle then the bald eagle chases the tiger.
((("something" "visits" "bald eagle" "+")) -> ("bald eagle" "chases" "tiger" "+"))
If the cat is not rough and the cat does not chase the tiger then the cat is blue.
((("cat" "is" "rough" "~") ("cat" "chases" "tiger" "~")) -> ("cat" "is" "blue" "+"))
If something chases the tiger then it is kind.
((("something" "chases" "tiger" "+")) -> ("something" "is" "kind" "+"))
If something is kind and it does not like the rabbit then it does not visit the rabbit.
((("something" "is" "kind" "+") ("something" "likes" "rabbit" "~")) -> ("something" "visits" "rabbit" "-"))
If something likes the cat and it is nice then it chases the cat.
((("something" "likes" "cat" "+") ("something" "is" "nice" "+")) -> ("something" "chases" "cat" "+"))
The bald eagle chases the cat.
True
1
proof
[(triple1)]
("bald eagle" "chases" "cat" "+")
triple1
The bald eagle is red.
False
1
inv-proof
[(triple2)]
("bald eagle" "is" "red" "+")
triple2
The bald eagle chases the tiger.
True
2
proof
[(((triple7) -> rule4))]
("bald eagle" "chases" "tiger" "+")
((triple7) -> (rule4 % int1))
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int1
The bald eagle does not chase the tiger.
False
2
inv-proof
[(((triple7) -> rule4))]
("bald eagle" "chases" "tiger" "-")
((triple7) -> (rule4 % int1))
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int1
The bald eagle is kind.
True
3
proof
[(((((triple7) -> rule4)) -> rule6))]
("bald eagle" "is" "kind" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int2
The bald eagle is not kind.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule6))]
("bald eagle" "is" "kind" "-")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int2
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "red" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "kind" "+")
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "blue" "-")
The tiger chases the bald eagle.
Unknown
random
[@0: The tiger chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bald eagle" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit likes the bald eagle.
Unknown
random
[@0: The rabbit likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bald eagle" "+")
@0: The bald eagle chases the cat.[(triple1)] The bald eagle is not red.[(triple2)] The bald eagle visits the tiger.[(triple3)] The cat does not chase the tiger.[(triple4)] The cat does not like the bald eagle.[(triple6)] The cat is rough.[(triple5)] The cat visits the bald eagle.[(triple7)] The cat visits the rabbit.[(triple8)] The rabbit chases the bald eagle.[(triple9)] The tiger chases the cat.[(triple10)] @1: The bald eagle chases the tiger.[(((triple7) -> rule4))] @2: The bald eagle is kind.[(((((triple7) -> rule4)) -> rule6))]
The bald eagle chases the cat.
("bald eagle" "chases" "cat" "+")
triple1
The bald eagle is not red.
("bald eagle" "is" "red" "-")
triple2
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
triple3
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
triple4
The cat does not like the bald eagle.
("cat" "likes" "bald eagle" "-")
triple6
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
triple7
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple8
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
triple9
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple10
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
((triple7) -> (rule4 % int1))
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int2