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