The bald eagle eats the dog. The bald eagle needs the cow. The bald eagle visits the dog. The bald eagle visits the tiger. The cow is blue. The cow visits the dog. The dog eats the bald eagle. The dog eats the cow. The dog is not green. The dog is young. The dog needs the tiger. The dog does not visit the bald eagle. The dog visits the cow. The dog visits the tiger. The tiger eats the cow. The tiger is not kind. If something needs the dog and it visits the dog then the dog visits the cow. If something visits the dog then it is cold. If something needs the tiger and the tiger visits the bald eagle then the tiger is not blue. If something is young then it visits the cow. If something is blue and it eats the tiger then the tiger visits the dog. If something is cold then it eats the tiger. If something eats the dog and it does not need the cow then it is not kind. Green things are young. If something needs the bald eagle and it visits the tiger then the bald eagle is blue.
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is not green.
("dog" "is" "green" "-")
The dog is young.
("dog" "is" "young" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog does not visit the bald eagle.
("dog" "visits" "bald eagle" "-")
The dog visits the cow.
("dog" "visits" "cow" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
If something needs the dog and it visits the dog then the dog visits the cow.
((("something" "needs" "dog" "+") ("something" "visits" "dog" "+")) -> ("dog" "visits" "cow" "+"))
If something visits the dog then it is cold.
((("something" "visits" "dog" "+")) -> ("something" "is" "cold" "+"))
If something needs the tiger and the tiger visits the bald eagle then the tiger is not blue.
((("something" "needs" "tiger" "+") ("tiger" "visits" "bald eagle" "+")) -> ("tiger" "is" "blue" "-"))
If something is young then it visits the cow.
((("something" "is" "young" "+")) -> ("something" "visits" "cow" "+"))
If something is blue and it eats the tiger then the tiger visits the dog.
((("something" "is" "blue" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If something is cold then it eats the tiger.
((("something" "is" "cold" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the dog and it does not need the cow then it is not kind.
((("something" "eats" "dog" "+") ("something" "needs" "cow" "~")) -> ("something" "is" "kind" "-"))
Green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something needs the bald eagle and it visits the tiger then the bald eagle is blue.
((("something" "needs" "bald eagle" "+") ("something" "visits" "tiger" "+")) -> ("bald eagle" "is" "blue" "+"))
The dog visits the tiger.
True
1
proof
[(triple14)]
("dog" "visits" "tiger" "+")
triple14
The dog is not young.
False
1
inv-proof
[(triple10)]
("dog" "is" "young" "-")
triple10
The bald eagle is cold.
True
2
proof
[(((triple3) -> rule2))]
("bald eagle" "is" "cold" "+")
((triple3) -> (rule2 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle is not cold.
False
2
inv-proof
[(((triple3) -> rule2))]
("bald eagle" "is" "cold" "-")
((triple3) -> (rule2 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The cow eats the tiger.
True
3
proof
[(((((triple6) -> rule2)) -> rule6))]
("cow" "eats" "tiger" "+")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The bald eagle does not eat the tiger.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6))]
("bald eagle" "eats" "tiger" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle eats the tiger.
("bald eagle" "eats" "tiger" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The tiger visits the dog.
True
5
proof
[(((triple5 ((((triple6) -> rule2)) -> rule6)) -> rule5))]
("tiger" "visits" "dog" "+")
((triple5 ((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The tiger does not visit the dog.
False
5
inv-proof
[(((triple5 ((((triple6) -> rule2)) -> rule6)) -> rule5))]
("tiger" "visits" "dog" "-")
((triple5 ((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The tiger is cold.
True
6
proof
[(((((triple5 ((((triple6) -> rule2)) -> rule6)) -> rule5)) -> rule2))]
("tiger" "is" "cold" "+")
((((triple5 ((((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The tiger is not cold.
False
6
inv-proof
[(((((triple5 ((((triple6) -> rule2)) -> rule6)) -> rule5)) -> rule2))]
("tiger" "is" "cold" "-")
((((triple5 ((((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The tiger eats the tiger.
True
7
proof
[(((((((triple5 ((((triple6) -> rule2)) -> rule6)) -> rule5)) -> rule2)) -> rule6))]
("tiger" "eats" "tiger" "+")
((((((triple5 ((((triple6) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5
The tiger does not eat the tiger.
False
7
inv-proof
[(((((((triple5 ((((triple6) -> rule2)) -> rule6)) -> rule5)) -> rule2)) -> rule6))]
("tiger" "eats" "tiger" "-")
((((((triple5 ((((triple6) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5
The bald eagle does not visit the cow.
Unknown
inv-rconc
[@2: The bald eagle visits the cow.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("bald eagle" "visits" "cow" "-")
The cow visits the cow.
Unknown
rconc
[@2: The cow visits the cow.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("cow" "visits" "cow" "+")
The tiger does not visit the cow.
Unknown
inv-rconc
[@2: The tiger visits the cow.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("tiger" "visits" "cow" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "young" "+")
The dog does not eat the tiger.
Unknown
inv-rconc
[@2: The dog eats the tiger.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("dog" "eats" "tiger" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "cold" "+")
The tiger does not need the dog.
Unknown
inv-random
[@0: The tiger needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "dog" "-")
The tiger eats the bald eagle.
Unknown
random
[@0: The tiger eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "bald eagle" "+")
The dog does not need the bald eagle.
Unknown
inv-random
[@0: The dog needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "bald eagle" "-")
The tiger eats the dog.
Unknown
random
[@0: The tiger eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "dog" "+")
The tiger does not visit the bald eagle.
Unknown
inv-random
[@0: The tiger visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "bald eagle" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The bald eagle eats the dog.[(triple1)] The bald eagle needs the cow.[(triple2)] The bald eagle visits the dog.[(triple3)] The bald eagle visits the tiger.[(triple4)] The cow is blue.[(triple5)] The cow visits the dog.[(triple6)] The dog does not visit the bald eagle.[(triple12)] The dog eats the bald eagle.[(triple7)] The dog eats the cow.[(triple8)] The dog is not green.[(triple9)] The dog is young.[(triple10)] The dog needs the tiger.[(triple11)] The dog visits the cow.[(triple13 OR ((triple10) -> rule4))] The dog visits the tiger.[(triple14)] The tiger eats the cow.[(triple15)] The tiger is not kind.[(triple16)] @1: The bald eagle is cold.[(((triple3) -> rule2))] The cow is cold.[(((triple6) -> rule2))] @2: The bald eagle eats the tiger.[(((((triple3) -> rule2)) -> rule6))] The cow eats the tiger.[(((((triple6) -> rule2)) -> rule6))] @3: The tiger visits the dog.[(((triple5 ((((triple6) -> rule2)) -> rule6)) -> rule5))] @4: The tiger is cold.[(((((triple5 ((((triple6) -> rule2)) -> rule6)) -> rule5)) -> rule2))] @5: The tiger eats the tiger.[(((((((triple5 ((((triple6) -> rule2)) -> rule6)) -> rule5)) -> rule2)) -> rule6))]
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
triple1
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
triple2
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
triple3
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
triple4
The cow is blue.
("cow" "is" "blue" "+")
triple5
The cow visits the dog.
("cow" "visits" "dog" "+")
triple6
The dog does not visit the bald eagle.
("dog" "visits" "bald eagle" "-")
triple12
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
triple7
The dog eats the cow.
("dog" "eats" "cow" "+")
triple8
The dog is not green.
("dog" "is" "green" "-")
triple9
The dog is young.
("dog" "is" "young" "+")
triple10
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple11
The dog visits the cow.
("dog" "visits" "cow" "+")
triple13
((triple10) -> (rule4 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple14
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple15
The tiger is not kind.
("tiger" "is" "kind" "-")
triple16
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
((triple3) -> (rule2 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple6) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The bald eagle eats the tiger.
("bald eagle" "eats" "tiger" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle eats the tiger.
("bald eagle" "eats" "tiger" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((triple5 ((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple5 ((((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((((triple5 ((((triple6) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5