The bald eagle visits the bear. The bear likes the cat. The cat visits the bear. The dog eats the bear. If the bear likes the bald eagle then the bear is cold. If something likes the dog and the dog does not visit the bear then the dog does not visit the cat. If something likes the cat then it does not visit the bald eagle. If something is round then it likes the cat. If something likes the cat then the cat is round. If something likes the cat then the cat is round. If something eats the dog and the dog is not round then it is cold. If the cat visits the bald eagle then the bald eagle likes the cat.
The bald eagle visits the bear.
("bald eagle" "visits" "bear" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The dog eats the bear.
("dog" "eats" "bear" "+")
If the bear likes the bald eagle then the bear is cold.
((("bear" "likes" "bald eagle" "+")) -> ("bear" "is" "cold" "+"))
If something likes the dog and the dog does not visit the bear then the dog does not visit the cat.
((("something" "likes" "dog" "+") ("dog" "visits" "bear" "~")) -> ("dog" "visits" "cat" "-"))
If something likes the cat then it does not visit the bald eagle.
((("something" "likes" "cat" "+")) -> ("something" "visits" "bald eagle" "-"))
If something is round then it likes the cat.
((("something" "is" "round" "+")) -> ("something" "likes" "cat" "+"))
If something likes the cat then the cat is round.
((("something" "likes" "cat" "+")) -> ("cat" "is" "round" "+"))
If something likes the cat then the cat is round.
((("something" "likes" "cat" "+")) -> ("cat" "is" "round" "+"))
If something eats the dog and the dog is not round then it is cold.
((("something" "eats" "dog" "+") ("dog" "is" "round" "~")) -> ("something" "is" "cold" "+"))
If the cat visits the bald eagle then the bald eagle likes the cat.
((("cat" "visits" "bald eagle" "+")) -> ("bald eagle" "likes" "cat" "+"))
The cat visits the bear.
True
1
proof
[(triple3)]
("cat" "visits" "bear" "+")
triple3
The bear does not like the cat.
False
1
inv-proof
[(triple2)]
("bear" "likes" "cat" "-")
triple2
The bear does not visit the bald eagle.
True
2
proof
[(((triple2) -> rule3))]
("bear" "visits" "bald eagle" "-")
((triple2) -> (rule3 % int1))
The bear does not visit the bald eagle.
("bear" "visits" "bald eagle" "-")
int1
The cat is not round.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple2) -> rule6))]
("cat" "is" "round" "-")
((triple2) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple2) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the cat.
True
3
proof
[(((((triple2) -> rule5)) -> rule4) OR ((((triple2) -> rule6)) -> rule4))]
("cat" "likes" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not like the cat.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule4) OR ((((triple2) -> rule6)) -> rule4))]
("cat" "likes" "cat" "-")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not visit the bald eagle.
True
4
proof
[(((((((triple2) -> rule5)) -> rule4)) -> rule3) OR ((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("cat" "visits" "bald eagle" "-")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat does not visit the bald eagle.
("cat" "visits" "bald eagle" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat does not visit the bald eagle.
("cat" "visits" "bald eagle" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat visits the bald eagle.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule4)) -> rule3) OR ((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("cat" "visits" "bald eagle" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat does not visit the bald eagle.
("cat" "visits" "bald eagle" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat does not visit the bald eagle.
("cat" "visits" "bald eagle" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bald eagle does not like the cat.
Unknown
inv-rconc
[@1: The bald eagle likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "likes" "cat" "-")
The dog likes the cat.
Unknown
rconc
[@1: The dog likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "likes" "cat" "+")
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "cold" "-")
The bald eagle is cold.
Unknown
rconc
[@1: The bald eagle is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "is" "cold" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The dog eats the bald eagle.
Unknown
random
[@0: The dog eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "bald eagle" "+")
The cat does not like the bear.
Unknown
inv-random
[@0: The cat likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "bear" "-")
The bear eats the bald eagle.
Unknown
random
[@0: The bear eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bald eagle" "+")
@0: The bald eagle visits the bear.[(triple1)] The bear likes the cat.[(triple2)] The cat visits the bear.[(triple3)] The dog eats the bear.[(triple4)] @1: The bear does not visit the bald eagle.[(((triple2) -> rule3))] The cat is round.[(((triple2) -> rule5) OR ((triple2) -> rule6))] @2: The cat likes the cat.[(((((triple2) -> rule5)) -> rule4) OR ((((triple2) -> rule6)) -> rule4))] @3: The cat does not visit the bald eagle.[(((((((triple2) -> rule5)) -> rule4)) -> rule3) OR ((((((triple2) -> rule6)) -> rule4)) -> rule3))]
The bald eagle visits the bear.
("bald eagle" "visits" "bear" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
The cat visits the bear.
("cat" "visits" "bear" "+")
triple3
The dog eats the bear.
("dog" "eats" "bear" "+")
triple4
The bear does not visit the bald eagle.
("bear" "visits" "bald eagle" "-")
((triple2) -> (rule3 % int1))
The bear does not visit the bald eagle.
("bear" "visits" "bald eagle" "-")
int1
The cat is round.
("cat" "is" "round" "+")
((triple2) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple2) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not visit the bald eagle.
("cat" "visits" "bald eagle" "-")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat does not visit the bald eagle.
("cat" "visits" "bald eagle" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat does not visit the bald eagle.
("cat" "visits" "bald eagle" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3