The cow visits the tiger. The mouse is blue. The tiger visits the cow. If something likes the cow and the cow needs the mouse then the mouse visits the tiger. If something is nice then it needs the cow. If something is nice then it visits the tiger. If something visits the tiger then the tiger visits the mouse. If something visits the mouse then it likes the mouse. If something visits the cow and it is big then it likes the cow. If something visits the mouse then it is nice. If something needs the cow and it is big then it needs the tiger.
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something likes the cow and the cow needs the mouse then the mouse visits the tiger.
((("something" "likes" "cow" "+") ("cow" "needs" "mouse" "+")) -> ("mouse" "visits" "tiger" "+"))
If something is nice then it needs the cow.
((("something" "is" "nice" "+")) -> ("something" "needs" "cow" "+"))
If something is nice then it visits the tiger.
((("something" "is" "nice" "+")) -> ("something" "visits" "tiger" "+"))
If something visits the tiger then the tiger visits the mouse.
((("something" "visits" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If something visits the mouse then it likes the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If something visits the cow and it is big then it likes the cow.
((("something" "visits" "cow" "+") ("something" "is" "big" "+")) -> ("something" "likes" "cow" "+"))
If something visits the mouse then it is nice.
((("something" "visits" "mouse" "+")) -> ("something" "is" "nice" "+"))
If something needs the cow and it is big then it needs the tiger.
((("something" "needs" "cow" "+") ("something" "is" "big" "+")) -> ("something" "needs" "tiger" "+"))
The cow visits the tiger.
True
1
proof
[(triple1)]
("cow" "visits" "tiger" "+")
triple1
The tiger does not visit the cow.
False
1
inv-proof
[(triple3)]
("tiger" "visits" "cow" "-")
triple3
The tiger visits the mouse.
True
2
proof
[(((triple1) -> rule4))]
("tiger" "visits" "mouse" "+")
((triple1) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger does not visit the mouse.
False
2
inv-proof
[(((triple1) -> rule4))]
("tiger" "visits" "mouse" "-")
((triple1) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger likes the mouse.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("tiger" "likes" "mouse" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The tiger does not like the mouse.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("tiger" "likes" "mouse" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The tiger visits the tiger.
True
4
proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule3))]
("tiger" "visits" "tiger" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int3
The tiger does not need the cow.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule2))]
("tiger" "needs" "cow" "-")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int3
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "nice" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "nice" "+")
The mouse does not need the tiger.
Unknown
inv-rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "needs" "tiger" "-")
The cow likes the mouse.
Unknown
rconc
[@1: The cow likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "likes" "mouse" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The cow needs the mouse.
Unknown
random
[@0: The cow needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "mouse" "+")
@0: The cow visits the tiger.[(triple1)] The mouse is blue.[(triple2)] The tiger visits the cow.[(triple3)] @1: The tiger visits the mouse.[(((triple1) -> rule4))] @2: The tiger is nice.[(((((triple1) -> rule4)) -> rule7))] The tiger likes the mouse.[(((((triple1) -> rule4)) -> rule5))] @3: The tiger needs the cow.[(((((((triple1) -> rule4)) -> rule7)) -> rule2))] The tiger visits the tiger.[(((((((triple1) -> rule4)) -> rule7)) -> rule3))]
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple3
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((triple1) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int3