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