The cow likes the mouse. The cow sees the rabbit. The mouse chases the cow. The mouse is big. The mouse sees the rabbit. The mouse sees the tiger. The rabbit is big. The rabbit likes the cow. The tiger likes the mouse. The tiger sees the rabbit. If someone chases the mouse then they like the rabbit. If the cow sees the rabbit then the cow sees the mouse. If someone is big then they chase the mouse. If someone likes the cow then they see the cow. If someone chases the mouse then the mouse likes the cow. If someone sees the cow and they see the mouse then the cow likes the mouse.
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone chases the mouse then they like the rabbit.
((("someone" "chases" "mouse" "+")) -> ("someone" "likes" "rabbit" "+"))
If the cow sees the rabbit then the cow sees the mouse.
((("cow" "sees" "rabbit" "+")) -> ("cow" "sees" "mouse" "+"))
If someone is big then they chase the mouse.
((("someone" "is" "big" "+")) -> ("someone" "chases" "mouse" "+"))
If someone likes the cow then they see the cow.
((("someone" "likes" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If someone chases the mouse then the mouse likes the cow.
((("someone" "chases" "mouse" "+")) -> ("mouse" "likes" "cow" "+"))
If someone sees the cow and they see the mouse then the cow likes the mouse.
((("someone" "sees" "cow" "+") ("someone" "sees" "mouse" "+")) -> ("cow" "likes" "mouse" "+"))
The cow likes the mouse.
True
1
proof
[(triple1)]
("cow" "likes" "mouse" "+")
triple1
The rabbit is not big.
False
1
inv-proof
[(triple7)]
("rabbit" "is" "big" "-")
triple7
The cow sees the mouse.
True
2
proof
[(((triple2) -> rule2))]
("cow" "sees" "mouse" "+")
((triple2) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The rabbit does not see the cow.
False
2
inv-proof
[(((triple8) -> rule4))]
("rabbit" "sees" "cow" "-")
((triple8) -> (rule4 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The mouse likes the cow.
True
3
proof
[(((((triple4) -> rule3)) -> rule5) OR ((((triple7) -> rule3)) -> rule5))]
("mouse" "likes" "cow" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The rabbit does not like the rabbit.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule1))]
("rabbit" "likes" "rabbit" "-")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The mouse sees the cow.
True
4
proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule4) OR ((((((triple7) -> rule3)) -> rule5)) -> rule4))]
("mouse" "sees" "cow" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The mouse does not see the cow.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule4) OR ((((((triple7) -> rule3)) -> rule5)) -> rule4))]
("mouse" "sees" "cow" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The tiger does not see the cow.
Unknown
inv-rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "cow" "-")
The tiger likes the rabbit.
Unknown
rconc
[@2: The tiger likes the rabbit.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("tiger" "likes" "rabbit" "+")
The cow does not chase the mouse.
Unknown
inv-rconc
[@1: The cow chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "chases" "mouse" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "sees" "cow" "+")
The rabbit does not like the tiger.
Unknown
inv-random
[@0: The rabbit likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "tiger" "-")
The tiger chases the rabbit.
Unknown
random
[@0: The tiger chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "rabbit" "+")
The mouse does not chase the tiger.
Unknown
inv-random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The cow likes the mouse.[(triple1)] The cow sees the rabbit.[(triple2)] The mouse chases the cow.[(triple3)] The mouse is big.[(triple4)] The mouse sees the rabbit.[(triple5)] The mouse sees the tiger.[(triple6)] The rabbit is big.[(triple7)] The rabbit likes the cow.[(triple8)] The tiger likes the mouse.[(triple9)] The tiger sees the rabbit.[(triple10)] @1: The cow sees the mouse.[(((triple2) -> rule2))] The mouse chases the mouse.[(((triple4) -> rule3))] The rabbit chases the mouse.[(((triple7) -> rule3))] The rabbit sees the cow.[(((triple8) -> rule4))] @2: The mouse likes the cow.[(((((triple4) -> rule3)) -> rule5) OR ((((triple7) -> rule3)) -> rule5))] The mouse likes the rabbit.[(((((triple4) -> rule3)) -> rule1))] The rabbit likes the rabbit.[(((((triple7) -> rule3)) -> rule1))] @3: The mouse sees the cow.[(((((((triple4) -> rule3)) -> rule5)) -> rule4) OR ((((((triple7) -> rule3)) -> rule5)) -> rule4))]
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple3
The mouse is big.
("mouse" "is" "big" "+")
triple4
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple5
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple6
The rabbit is big.
("rabbit" "is" "big" "+")
triple7
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple8
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((triple2) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple4) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((triple7) -> (rule3 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
((triple8) -> (rule4 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3