The bald eagle needs the tiger. The cow needs the tiger. The cow sees the tiger. The cow visits the tiger. The dog is nice. The dog needs the cow. The dog sees the bald eagle. The dog sees the cow. The tiger is blue. The tiger needs the cow. The tiger needs the dog. If someone visits the cow then they are blue. If someone visits the dog then they see the bald eagle. If someone is rough then they visit the bald eagle. If someone is blue then they visit the tiger. If someone needs the dog then the dog is rough. If someone visits the tiger then they visit the bald eagle. If someone visits the bald eagle and the bald eagle sees the tiger then they see the bald eagle. If someone sees the cow then they need the bald eagle. If someone needs the tiger and the tiger visits the bald eagle then they are blue.
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone visits the cow then they are blue.
((("someone" "visits" "cow" "+")) -> ("someone" "is" "blue" "+"))
If someone visits the dog then they see the bald eagle.
((("someone" "visits" "dog" "+")) -> ("someone" "sees" "bald eagle" "+"))
If someone is rough then they visit the bald eagle.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "bald eagle" "+"))
If someone is blue then they visit the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "tiger" "+"))
If someone needs the dog then the dog is rough.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "rough" "+"))
If someone visits the tiger then they visit the bald eagle.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "bald eagle" "+"))
If someone visits the bald eagle and the bald eagle sees the tiger then they see the bald eagle.
((("someone" "visits" "bald eagle" "+") ("bald eagle" "sees" "tiger" "+")) -> ("someone" "sees" "bald eagle" "+"))
If someone sees the cow then they need the bald eagle.
((("someone" "sees" "cow" "+")) -> ("someone" "needs" "bald eagle" "+"))
If someone needs the tiger and the tiger visits the bald eagle then they are blue.
((("someone" "needs" "tiger" "+") ("tiger" "visits" "bald eagle" "+")) -> ("someone" "is" "blue" "+"))
The tiger needs the dog.
True
1
proof
[(triple11)]
("tiger" "needs" "dog" "+")
triple11
The tiger is not blue.
False
1
inv-proof
[(triple9)]
("tiger" "is" "blue" "-")
triple9
The cow visits the bald eagle.
True
2
proof
[(((triple4) -> rule6) OR ((((((triple2 ((((triple9) -> rule4)) -> rule6)) -> rule9)) -> rule4)) -> rule6))]
("cow" "visits" "bald eagle" "+")
((triple4) -> (rule6 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1
((((((triple2 ((((triple9) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int5
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple9) -> rule4))]
("tiger" "visits" "tiger" "-")
((triple9) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The dog visits the bald eagle.
True
3
proof
[(((((triple11) -> rule5)) -> rule3))]
("dog" "visits" "bald eagle" "+")
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
The dog visits the bald eagle.
("dog" "visits" "bald eagle" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The tiger does not visit the bald eagle.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule6))]
("tiger" "visits" "bald eagle" "-")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The bald eagle is blue.
True
5
proof
[(((triple1 ((((triple9) -> rule4)) -> rule6)) -> rule9))]
("bald eagle" "is" "blue" "+")
((triple1 ((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The cow is not blue.
False
5
inv-proof
[(((triple2 ((((triple9) -> rule4)) -> rule6)) -> rule9))]
("cow" "is" "blue" "-")
((triple2 ((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The bald eagle visits the tiger.
True
6
proof
[(((((triple1 ((((triple9) -> rule4)) -> rule6)) -> rule9)) -> rule4))]
("bald eagle" "visits" "tiger" "+")
((((triple1 ((((triple9) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4
The bald eagle does not visit the tiger.
False
6
inv-proof
[(((((triple1 ((((triple9) -> rule4)) -> rule6)) -> rule9)) -> rule4))]
("bald eagle" "visits" "tiger" "-")
((((triple1 ((((triple9) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4
The bald eagle visits the bald eagle.
True
7
proof
[(((((((triple1 ((((triple9) -> rule4)) -> rule6)) -> rule9)) -> rule4)) -> rule6))]
("bald eagle" "visits" "bald eagle" "+")
((((((triple1 ((((triple9) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int3
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int5
The bald eagle does not visit the bald eagle.
False
7
inv-proof
[(((((((triple1 ((((triple9) -> rule4)) -> rule6)) -> rule9)) -> rule4)) -> rule6))]
("bald eagle" "visits" "bald eagle" "-")
((((((triple1 ((((triple9) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int3
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int5
The bald eagle does not see the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The tiger sees the bald eagle.
Unknown
rconc
[@1: The tiger sees the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "bald eagle" "+")
The bald eagle does not need the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The cow sees the bald eagle.
Unknown
rconc
[@1: The cow sees the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "bald eagle" "+")
The cow does not need the bald eagle.
Unknown
inv-rconc
[@1: The cow needs the bald eagle.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "needs" "bald eagle" "-")
The dog visits the tiger.
Unknown
rconc
[@2: The dog visits the tiger.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("dog" "visits" "tiger" "+")
The tiger does not visit the cow.
Unknown
inv-random
[@0: The tiger visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cow" "-")
The tiger sees the cow.
Unknown
random
[@0: The tiger sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cow" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The dog does not need the tiger.
Unknown
inv-random
[@0: The dog needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "tiger" "-")
The cow visits the dog.
Unknown
random
[@0: The cow visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "dog" "+")
@0: The bald eagle needs the tiger.[(triple1)] The cow needs the tiger.[(triple2)] The cow sees the tiger.[(triple3)] The cow visits the tiger.[(triple4 OR ((((triple2 ((((triple9) -> rule4)) -> rule6)) -> rule9)) -> rule4))] The dog is nice.[(triple5)] The dog needs the cow.[(triple6)] The dog sees the bald eagle.[(triple7)] The dog sees the cow.[(triple8)] The tiger is blue.[(triple9)] The tiger needs the cow.[(triple10)] The tiger needs the dog.[(triple11)] @1: The cow visits the bald eagle.[(((triple4) -> rule6) OR ((((((triple2 ((((triple9) -> rule4)) -> rule6)) -> rule9)) -> rule4)) -> rule6))] The dog is rough.[(((triple11) -> rule5))] The dog needs the bald eagle.[(((triple8) -> rule8))] The tiger visits the tiger.[(((triple9) -> rule4))] @2: The dog visits the bald eagle.[(((((triple11) -> rule5)) -> rule3))] The tiger visits the bald eagle.[(((((triple9) -> rule4)) -> rule6))] @3: The bald eagle is blue.[(((triple1 ((((triple9) -> rule4)) -> rule6)) -> rule9))] The cow is blue.[(((triple2 ((((triple9) -> rule4)) -> rule6)) -> rule9))] @4: The bald eagle visits the tiger.[(((((triple1 ((((triple9) -> rule4)) -> rule6)) -> rule9)) -> rule4))] @5: The bald eagle visits the bald eagle.[(((((((triple1 ((((triple9) -> rule4)) -> rule6)) -> rule9)) -> rule4)) -> rule6))]
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple3
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple4
((((triple2 ((((triple9) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4
The dog is nice.
("dog" "is" "nice" "+")
triple5
The dog needs the cow.
("dog" "needs" "cow" "+")
triple6
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
triple7
The dog sees the cow.
("dog" "sees" "cow" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple10
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple11
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
((triple4) -> (rule6 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1
((((((triple2 ((((triple9) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int5
The dog is rough.
("dog" "is" "rough" "+")
((triple11) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
((triple8) -> (rule8 % int1))
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple9) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The dog visits the bald eagle.
("dog" "visits" "bald eagle" "+")
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
The dog visits the bald eagle.
("dog" "visits" "bald eagle" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
((triple1 ((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
((triple2 ((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
((((triple1 ((((triple9) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
((((((triple1 ((((triple9) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int3
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int5