The cow does not eat the mouse. The cow eats the tiger. The cow is big. The cow likes the tiger. The mouse eats the cow. The mouse is not big. The mouse is kind. The mouse is rough. The mouse likes the tiger. The tiger is green. The tiger is nice. The tiger likes the cow. The tiger does not like the mouse. The tiger needs the cow. The tiger needs the mouse. If something needs the mouse then it is nice. If the mouse eats the tiger and the tiger eats the cow then the tiger needs the cow. If something eats the cow and it needs the cow then the cow needs the tiger. If something eats the cow and the cow likes the mouse then the cow needs the tiger. If something is nice and kind then it likes the mouse. If something is nice then it needs the cow. If the cow likes the tiger and the cow is big then the cow needs the mouse. If the mouse needs the tiger and the tiger does not need the cow then the cow is not green.
The cow does not eat the mouse.
("cow" "eats" "mouse" "-")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is big.
("cow" "is" "big" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something needs the mouse then it is nice.
((("something" "needs" "mouse" "+")) -> ("something" "is" "nice" "+"))
If the mouse eats the tiger and the tiger eats the cow then the tiger needs the cow.
((("mouse" "eats" "tiger" "+") ("tiger" "eats" "cow" "+")) -> ("tiger" "needs" "cow" "+"))
If something eats the cow and it needs the cow then the cow needs the tiger.
((("something" "eats" "cow" "+") ("something" "needs" "cow" "+")) -> ("cow" "needs" "tiger" "+"))
If something eats the cow and the cow likes the mouse then the cow needs the tiger.
((("something" "eats" "cow" "+") ("cow" "likes" "mouse" "+")) -> ("cow" "needs" "tiger" "+"))
If something is nice and kind then it likes the mouse.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "likes" "mouse" "+"))
If something is nice then it needs the cow.
((("something" "is" "nice" "+")) -> ("something" "needs" "cow" "+"))
If the cow likes the tiger and the cow is big then the cow needs the mouse.
((("cow" "likes" "tiger" "+") ("cow" "is" "big" "+")) -> ("cow" "needs" "mouse" "+"))
If the mouse needs the tiger and the tiger does not need the cow then the cow is not green.
((("mouse" "needs" "tiger" "+") ("tiger" "needs" "cow" "~")) -> ("cow" "is" "green" "-"))
The cow likes the tiger.
True
1
proof
[(triple4)]
("cow" "likes" "tiger" "+")
triple4
The mouse does not eat the cow.
False
1
inv-proof
[(triple5)]
("mouse" "eats" "cow" "-")
triple5
The cow needs the mouse.
True
3
proof
[(((triple4 triple3) -> rule7))]
("cow" "needs" "mouse" "+")
((triple4 triple3) -> (rule7 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow does not need the mouse.
False
3
inv-proof
[(((triple4 triple3) -> rule7))]
("cow" "needs" "mouse" "-")
((triple4 triple3) -> (rule7 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow is nice.
True
4
proof
[(((((triple4 triple3) -> rule7)) -> rule1))]
("cow" "is" "nice" "+")
((((triple4 triple3) -> (rule7 % int2))) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow is not nice.
False
4
inv-proof
[(((((triple4 triple3) -> rule7)) -> rule1))]
("cow" "is" "nice" "-")
((((triple4 triple3) -> (rule7 % int2))) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow needs the cow.
True
5
proof
[(((((((triple4 triple3) -> rule7)) -> rule1)) -> rule6))]
("cow" "needs" "cow" "+")
((((((triple4 triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The cow does not need the cow.
False
5
inv-proof
[(((((((triple4 triple3) -> rule7)) -> rule1)) -> rule6))]
("cow" "needs" "cow" "-")
((((((triple4 triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The mouse does not need the cow.
Unknown
inv-rconc
[@2: The mouse needs the cow.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("mouse" "needs" "cow" "-")
The cow needs the tiger.
Unknown
rconc
[@3: The cow needs the tiger.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("cow" "needs" "tiger" "+")
The mouse does not like the mouse.
Unknown
inv-rconc
[@2: The mouse likes the mouse.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "nice" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The cow does not eat the mouse.[(triple1)] The cow eats the tiger.[(triple2)] The cow is big.[(triple3)] The cow likes the tiger.[(triple4)] The mouse eats the cow.[(triple5)] The mouse is kind.[(triple7)] The mouse is not big.[(triple6)] The mouse is rough.[(triple8)] The mouse likes the tiger.[(triple9)] The tiger does not like the mouse.[(triple13)] The tiger is green.[(triple10)] The tiger is nice.[(triple11 OR ((triple15) -> rule1))] The tiger likes the cow.[(triple12)] The tiger needs the cow.[(triple14 OR ((triple11) -> rule6) OR ((((triple15) -> rule1)) -> rule6))] The tiger needs the mouse.[(triple15)] @1: The cow needs the mouse.[(((triple4 triple3) -> rule7))] @2: The cow is nice.[(((((triple4 triple3) -> rule7)) -> rule1))] @3: The cow needs the cow.[(((((((triple4 triple3) -> rule7)) -> rule1)) -> rule6))]
The cow does not eat the mouse.
("cow" "eats" "mouse" "-")
triple1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple4
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple5
The mouse is kind.
("mouse" "is" "kind" "+")
triple7
The mouse is not big.
("mouse" "is" "big" "-")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple8
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple9
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
triple13
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
((triple15) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple12
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple14
((triple11) -> (rule6 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule6 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple15
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple4 triple3) -> (rule7 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((((triple4 triple3) -> (rule7 % int2))) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((triple4 triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3