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