The mouse is green. The tiger likes the mouse. If the tiger likes the mouse then the tiger does not chase the mouse. If something is kind then it does not like the mouse. If something likes the mouse then the mouse is kind. If the tiger chases the mouse and the mouse likes the tiger then the tiger is not red. If the tiger does not chase the mouse then the mouse chases the tiger. If something chases the tiger then it is red. If something is big then it is red. If something is red then it does not eat the tiger.
The mouse is green.
("mouse" "is" "green" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If the tiger likes the mouse then the tiger does not chase the mouse.
((("tiger" "likes" "mouse" "+")) -> ("tiger" "chases" "mouse" "-"))
If something is kind then it does not like the mouse.
((("something" "is" "kind" "+")) -> ("something" "likes" "mouse" "-"))
If something likes the mouse then the mouse is kind.
((("something" "likes" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If the tiger chases the mouse and the mouse likes the tiger then the tiger is not red.
((("tiger" "chases" "mouse" "+") ("mouse" "likes" "tiger" "+")) -> ("tiger" "is" "red" "-"))
If the tiger does not chase the mouse then the mouse chases the tiger.
((("tiger" "chases" "mouse" "~")) -> ("mouse" "chases" "tiger" "+"))
If something chases the tiger then it is red.
((("something" "chases" "tiger" "+")) -> ("something" "is" "red" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is red then it does not eat the tiger.
((("something" "is" "red" "+")) -> ("something" "eats" "tiger" "-"))
The mouse is green.
True
1
proof
[(triple1)]
("mouse" "is" "green" "+")
triple1
The mouse is not green.
False
1
inv-proof
[(triple1)]
("mouse" "is" "green" "-")
triple1
The mouse is kind.
True
2
proof
[(((triple2) -> rule3))]
("mouse" "is" "kind" "+")
((triple2) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "is" "kind" "-")
((triple2) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse does not like the mouse.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("mouse" "likes" "mouse" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the mouse.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("mouse" "likes" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is red.
True
4
proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule6))]
("mouse" "is" "red" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
int3
The mouse is not red.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule6))]
("mouse" "is" "red" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
int3
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "red" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The mouse does not like the tiger.
Unknown
inv-random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The mouse is green.[(triple1)] The tiger likes the mouse.[(triple2)] @1: The mouse is kind.[(((triple2) -> rule3))] The tiger does not chase the mouse.[(((triple2) -> rule1))] @2: The mouse chases the tiger.[(((((triple2) -> rule1)) -> rule5))] The mouse does not like the mouse.[(((((triple2) -> rule3)) -> rule2))] @3: The mouse is red.[(((((((triple2) -> rule1)) -> rule5)) -> rule6))] @4: The mouse does not eat the tiger.[(((((((((triple2) -> rule1)) -> rule5)) -> rule6)) -> rule8))]
The mouse is green.
("mouse" "is" "green" "+")
triple1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
((triple2) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
((triple2) -> (rule1 % int1))
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
int2
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
int3
The mouse does not eat the tiger.
("mouse" "eats" "tiger" "-")
((((((((triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The mouse does not eat the tiger.
("mouse" "eats" "tiger" "-")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int3
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
int4