The cow visits the tiger. The mouse visits the cow. The tiger eats the cow. The tiger eats the mouse. The tiger is big. The tiger likes the mouse. The tiger visits the mouse. If someone likes the mouse then they like the cow. If someone visits the mouse and they like the cow then the mouse eats the tiger. If someone eats the tiger then they are big. If someone eats the mouse and the mouse is blue then they like the cow. If someone likes the cow then they eat the cow. If someone visits the tiger and the tiger likes the cow then the cow eats the tiger.
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone likes the mouse then they like the cow.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "cow" "+"))
If someone visits the mouse and they like the cow then the mouse eats the tiger.
((("someone" "visits" "mouse" "+") ("someone" "likes" "cow" "+")) -> ("mouse" "eats" "tiger" "+"))
If someone eats the tiger then they are big.
((("someone" "eats" "tiger" "+")) -> ("someone" "is" "big" "+"))
If someone eats the mouse and the mouse is blue then they like the cow.
((("someone" "eats" "mouse" "+") ("mouse" "is" "blue" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the cow then they eat the cow.
((("someone" "likes" "cow" "+")) -> ("someone" "eats" "cow" "+"))
If someone visits the tiger and the tiger likes the cow then the cow eats the tiger.
((("someone" "visits" "tiger" "+") ("tiger" "likes" "cow" "+")) -> ("cow" "eats" "tiger" "+"))
The tiger likes the mouse.
True
1
proof
[(triple6)]
("tiger" "likes" "mouse" "+")
triple6
The mouse does not visit the cow.
False
1
inv-proof
[(triple2)]
("mouse" "visits" "cow" "-")
triple2
The tiger likes the cow.
True
2
proof
[(((triple6) -> rule1))]
("tiger" "likes" "cow" "+")
((triple6) -> (rule1 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger does not like the cow.
False
2
inv-proof
[(((triple6) -> rule1))]
("tiger" "likes" "cow" "-")
((triple6) -> (rule1 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The mouse eats the tiger.
True
4
proof
[(((triple7 ((triple6) -> rule1)) -> rule2))]
("mouse" "eats" "tiger" "+")
((triple7 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The mouse does not eat the tiger.
False
4
inv-proof
[(((triple7 ((triple6) -> rule1)) -> rule2))]
("mouse" "eats" "tiger" "-")
((triple7 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The mouse is big.
True
5
proof
[(((((triple7 ((triple6) -> rule1)) -> rule2)) -> rule3))]
("mouse" "is" "big" "+")
((((triple7 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The mouse is not big.
False
5
inv-proof
[(((((triple7 ((triple6) -> rule1)) -> rule2)) -> rule3))]
("mouse" "is" "big" "-")
((((triple7 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The mouse does not like the cow.
Unknown
inv-rconc
[@1: The mouse likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "cow" "-")
The mouse eats the cow.
Unknown
rconc
[@2: The mouse eats the cow.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("mouse" "eats" "cow" "+")
The cow does not eat the cow.
Unknown
inv-rconc
[@2: The cow eats the cow.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cow" "eats" "cow" "-")
The cow likes the cow.
Unknown
rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cow" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The cow visits the mouse.
Unknown
random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "+")
The cow does not like the tiger.
Unknown
inv-random
[@0: The cow likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "tiger" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cow visits the tiger.[(triple1)] The mouse visits the cow.[(triple2)] The tiger eats the cow.[(triple3 OR ((((triple6) -> rule1)) -> rule5))] The tiger eats the mouse.[(triple4)] The tiger is big.[(triple5)] The tiger likes the mouse.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The tiger likes the cow.[(((triple6) -> rule1))] @2: The cow eats the tiger.[(((triple1 ((triple6) -> rule1)) -> rule6))] The mouse eats the tiger.[(((triple7 ((triple6) -> rule1)) -> rule2))] @3: The cow is big.[(((((triple1 ((triple6) -> rule1)) -> rule6)) -> rule3))] The mouse is big.[(((((triple7 ((triple6) -> rule1)) -> rule2)) -> rule3))]
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple3
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The tiger likes the cow.
("tiger" "likes" "cow" "+")
((triple6) -> (rule1 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((triple1 ((triple6) -> (rule1 % int2))) -> (rule6 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((triple7 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((((triple1 ((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
((((triple7 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3