The cow is blue. The mouse is not round. The tiger likes the cow. If someone likes the mouse then they like the cow. If the mouse is blue then the mouse likes the cow. If someone eats the cow then they do not see the tiger. If someone is blue then they like the mouse. If someone eats the tiger then the tiger is blue. If the mouse sees the cow and the mouse is nice then the cow is nice.
The cow is blue.
("cow" "is" "blue" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If someone likes the mouse then they like the cow.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "cow" "+"))
If the mouse is blue then the mouse likes the cow.
((("mouse" "is" "blue" "+")) -> ("mouse" "likes" "cow" "+"))
If someone eats the cow then they do not see the tiger.
((("someone" "eats" "cow" "+")) -> ("someone" "sees" "tiger" "-"))
If someone is blue then they like the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "mouse" "+"))
If someone eats the tiger then the tiger is blue.
((("someone" "eats" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If the mouse sees the cow and the mouse is nice then the cow is nice.
((("mouse" "sees" "cow" "+") ("mouse" "is" "nice" "+")) -> ("cow" "is" "nice" "+"))
The mouse is not round.
True
1
proof
[(triple2)]
("mouse" "is" "round" "-")
triple2
The tiger does not like the cow.
False
1
inv-proof
[(triple3)]
("tiger" "likes" "cow" "-")
triple3
The cow likes the mouse.
True
2
proof
[(((triple1) -> rule4))]
("cow" "likes" "mouse" "+")
((triple1) -> (rule4 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow does not like the mouse.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "likes" "mouse" "-")
((triple1) -> (rule4 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow likes the cow.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("cow" "likes" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow does not like the cow.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("cow" "likes" "cow" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The mouse does not like the cow.
Unknown
inv-rconc
[@2: The mouse likes the cow.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("mouse" "likes" "cow" "-")
The tiger likes the mouse.
Unknown
rconc
[@2: The tiger likes the mouse.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("tiger" "likes" "mouse" "+")
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "nice" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
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 sees the tiger.
Unknown
random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "+")
@0: The cow is blue.[(triple1)] The mouse is not round.[(triple2)] The tiger likes the cow.[(triple3)] @1: The cow likes the mouse.[(((triple1) -> rule4))] @2: The cow likes the cow.[(((((triple1) -> rule4)) -> rule1))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The mouse is not round.
("mouse" "is" "round" "-")
triple2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((triple1) -> (rule4 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2