The bald eagle likes the tiger. The bald eagle sees the cow. The cow is red. The cow sees the tiger. The mouse eats the bald eagle. The mouse eats the cow. The mouse eats the tiger. The mouse is cold. The mouse likes the tiger. The tiger eats the bald eagle. The tiger eats the cow. The tiger is red. The tiger is young. The tiger likes the bald eagle. The tiger likes the mouse. The tiger sees the mouse. All nice people are kind. If someone is nice and they see the bald eagle then the bald eagle likes the mouse. If someone likes the cow then they are nice. If someone is nice and they like the mouse then the mouse sees the cow. If the mouse eats the tiger then the tiger sees the mouse. If someone likes the tiger and the tiger is young then the tiger likes the bald eagle. If someone is kind then they see the bald eagle. If someone eats the tiger then the tiger likes the cow.
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is nice and they see the bald eagle then the bald eagle likes the mouse.
((("someone" "is" "nice" "+") ("someone" "sees" "bald eagle" "+")) -> ("bald eagle" "likes" "mouse" "+"))
If someone likes the cow then they are nice.
((("someone" "likes" "cow" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and they like the mouse then the mouse sees the cow.
((("someone" "is" "nice" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
If the mouse eats the tiger then the tiger sees the mouse.
((("mouse" "eats" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If someone likes the tiger and the tiger is young then the tiger likes the bald eagle.
((("someone" "likes" "tiger" "+") ("tiger" "is" "young" "+")) -> ("tiger" "likes" "bald eagle" "+"))
If someone is kind then they see the bald eagle.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "bald eagle" "+"))
If someone eats the tiger then the tiger likes the cow.
((("someone" "eats" "tiger" "+")) -> ("tiger" "likes" "cow" "+"))
The bald eagle sees the cow.
True
1
proof
[(triple2)]
("bald eagle" "sees" "cow" "+")
triple2
The mouse does not like the tiger.
False
1
inv-proof
[(triple9)]
("mouse" "likes" "tiger" "-")
triple9
The tiger likes the cow.
True
2
proof
[(((triple7) -> rule8))]
("tiger" "likes" "cow" "+")
((triple7) -> (rule8 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger does not like the cow.
False
2
inv-proof
[(((triple7) -> rule8))]
("tiger" "likes" "cow" "-")
((triple7) -> (rule8 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger is nice.
True
3
proof
[(((((triple7) -> rule8)) -> rule3))]
("tiger" "is" "nice" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger is not nice.
False
3
inv-proof
[(((((triple7) -> rule8)) -> rule3))]
("tiger" "is" "nice" "-")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The mouse sees the cow.
True
5
proof
[(((((((triple7) -> rule8)) -> rule3) triple15) -> rule4))]
("mouse" "sees" "cow" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2)) triple15) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger is not kind.
False
4
inv-proof
[(((((((triple7) -> rule8)) -> rule3)) -> rule1))]
("tiger" "is" "kind" "-")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger sees the bald eagle.
True
5
proof
[(((((((((triple7) -> rule8)) -> rule3)) -> rule1)) -> rule7))]
("tiger" "sees" "bald eagle" "+")
((((((((triple7) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
The tiger does not see the bald eagle.
False
5
inv-proof
[(((((((((triple7) -> rule8)) -> rule3)) -> rule1)) -> rule7))]
("tiger" "sees" "bald eagle" "-")
((((((((triple7) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
The bald eagle likes the mouse.
True
9
proof
[(((((((triple7) -> rule8)) -> rule3) ((((((((triple7) -> rule8)) -> rule3)) -> rule1)) -> rule7)) -> rule2))]
("bald eagle" "likes" "mouse" "+")
((((((triple7) -> (rule8 % int5))) -> (rule3 % int4)) ((((((((triple7) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int5
The bald eagle does not like the mouse.
False
9
inv-proof
[(((((((triple7) -> rule8)) -> rule3) ((((((((triple7) -> rule8)) -> rule3)) -> rule1)) -> rule7)) -> rule2))]
("bald eagle" "likes" "mouse" "-")
((((((triple7) -> (rule8 % int5))) -> (rule3 % int4)) ((((((((triple7) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int5
The mouse is not kind.
Unknown
inv-rconc
[@2: The mouse is kind.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("mouse" "is" "kind" "-")
The cow is kind.
Unknown
rconc
[@2: The cow is kind.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("cow" "is" "kind" "+")
The bald eagle does not see the bald eagle.
Unknown
inv-rconc
[@3: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule3 <- FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "nice" "+")
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "nice" "-")
The cow sees the bald eagle.
Unknown
rconc
[@3: The cow sees the bald eagle.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule3 <- FAIL)]]
("cow" "sees" "bald eagle" "+")
The bald eagle does not eat the tiger.
Unknown
inv-random
[@0: The bald eagle eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "tiger" "-")
The bald eagle is young.
Unknown
random
[@0: The bald eagle is young.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "young" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The bald eagle sees the mouse.
Unknown
random
[@0: The bald eagle sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "mouse" "+")
The cow does not eat the tiger.
Unknown
inv-random
[@0: The cow eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "tiger" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The bald eagle likes the tiger.[(triple1)] The bald eagle sees the cow.[(triple2)] The cow is red.[(triple3)] The cow sees the tiger.[(triple4)] The mouse eats the bald eagle.[(triple5)] The mouse eats the cow.[(triple6)] The mouse eats the tiger.[(triple7)] The mouse is cold.[(triple8)] The mouse likes the tiger.[(triple9)] The tiger eats the bald eagle.[(triple10)] The tiger eats the cow.[(triple11)] The tiger is red.[(triple12)] The tiger is young.[(triple13)] The tiger likes the bald eagle.[(triple14 OR ((triple1 triple13) -> rule6) OR ((triple9 triple13) -> rule6))] The tiger likes the mouse.[(triple15)] The tiger sees the mouse.[(triple16 OR ((triple7) -> rule5))] @1: The tiger likes the cow.[(((triple7) -> rule8))] @2: The tiger is nice.[(((((triple7) -> rule8)) -> rule3))] @3: The mouse sees the cow.[(((((((triple7) -> rule8)) -> rule3) triple15) -> rule4))] The tiger is kind.[(((((((triple7) -> rule8)) -> rule3)) -> rule1))] @4: The tiger sees the bald eagle.[(((((((((triple7) -> rule8)) -> rule3)) -> rule1)) -> rule7))] @5: The bald eagle likes the mouse.[(((((((triple7) -> rule8)) -> rule3) ((((((((triple7) -> rule8)) -> rule3)) -> rule1)) -> rule7)) -> rule2))]
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
triple1
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple4
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
triple5
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple6
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple9
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
triple10
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple11
The tiger is red.
("tiger" "is" "red" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
triple14
((triple1 triple13) -> (rule6 % int1))
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
int1
((triple9 triple13) -> (rule6 % int1))
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple15
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple16
((triple7) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
((triple7) -> (rule8 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2)) triple15) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
((((((((triple7) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
((((((triple7) -> (rule8 % int5))) -> (rule3 % int4)) ((((((((triple7) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int5