The cow eats the tiger. The cow is cold. The cow likes the mouse. The cow likes the tiger. The mouse eats the cow. The mouse is blue. The mouse is round. The mouse is young. The mouse likes the tiger. The mouse needs the cow. The mouse needs the tiger. The tiger eats the cow. The tiger is blue. The tiger likes the cow. The tiger needs the cow. If someone is blue then they like the tiger. If someone eats the mouse then they are young. If someone likes the tiger then they eat the mouse.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If someone is blue then they like the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "tiger" "+"))
If someone eats the mouse then they are young.
((("someone" "eats" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone likes the tiger then they eat the mouse.
((("someone" "likes" "tiger" "+")) -> ("someone" "eats" "mouse" "+"))
The mouse needs the cow.
True
1
proof
[(triple10)]
("mouse" "needs" "cow" "+")
triple10
The mouse does not like the tiger.
False
1
inv-proof
[(triple9 OR ((triple6) -> rule1))]
("mouse" "likes" "tiger" "-")
triple9
((triple6) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The cow eats the mouse.
True
2
proof
[(((triple4) -> rule3))]
("cow" "eats" "mouse" "+")
((triple4) -> (rule3 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow does not eat the mouse.
False
2
inv-proof
[(((triple4) -> rule3))]
("cow" "eats" "mouse" "-")
((triple4) -> (rule3 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The tiger eats the mouse.
True
3
proof
[(((((triple13) -> rule1)) -> rule3))]
("tiger" "eats" "mouse" "+")
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The cow is not young.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("cow" "is" "young" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The tiger is young.
True
4
proof
[(((((((triple13) -> rule1)) -> rule3)) -> rule2))]
("tiger" "is" "young" "+")
((((((triple13) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is not young.
False
4
inv-proof
[(((((((triple13) -> rule1)) -> rule3)) -> rule2))]
("tiger" "is" "young" "-")
((((((triple13) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger does not like the mouse.
Unknown
inv-random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
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 tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The cow does not need the mouse.
Unknown
inv-random
[@0: The cow needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "mouse" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The mouse eats the tiger.
Unknown
random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "+")
@0: The cow eats the tiger.[(triple1)] The cow is cold.[(triple2)] The cow likes the mouse.[(triple3)] The cow likes the tiger.[(triple4)] The mouse eats the cow.[(triple5)] The mouse is blue.[(triple6)] The mouse is round.[(triple7)] The mouse is young.[(triple8 OR ((((triple9) -> rule3)) -> rule2) OR ((((((triple6) -> rule1)) -> rule3)) -> rule2))] The mouse likes the tiger.[(triple9 OR ((triple6) -> rule1))] The mouse needs the cow.[(triple10)] The mouse needs the tiger.[(triple11)] The tiger eats the cow.[(triple12)] The tiger is blue.[(triple13)] The tiger likes the cow.[(triple14)] The tiger needs the cow.[(triple15)] @1: The cow eats the mouse.[(((triple4) -> rule3))] The mouse eats the mouse.[(((triple9) -> rule3) OR ((((triple6) -> rule1)) -> rule3))] The tiger likes the tiger.[(((triple13) -> rule1))] @2: The cow is young.[(((((triple4) -> rule3)) -> rule2))] The tiger eats the mouse.[(((((triple13) -> rule1)) -> rule3))] @3: The tiger is young.[(((((((triple13) -> rule1)) -> rule3)) -> rule2))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple4
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse is round.
("mouse" "is" "round" "+")
triple7
The mouse is young.
("mouse" "is" "young" "+")
triple8
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple9
((triple6) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple10
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple11
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple12
The tiger is blue.
("tiger" "is" "blue" "+")
triple13
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple14
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple15
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((triple4) -> (rule3 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple9) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple13) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
((((((triple13) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3