The cat is red. The cat is rough. The mouse chases the cat. The mouse eats the cat. The mouse is not green. The mouse is not nice. The mouse needs the cat. If someone eats the mouse then the mouse is rough. All nice people are green. If someone needs the mouse and they do not need the cat then the cat chases the mouse. If someone is rough then they chase the mouse. If someone chases the cat then the cat eats the mouse. If someone is red and they do not chase the mouse then the mouse does not eat the cat.
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If someone eats the mouse then the mouse is rough.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone needs the mouse and they do not need the cat then the cat chases the mouse.
((("someone" "needs" "mouse" "+") ("someone" "needs" "cat" "~")) -> ("cat" "chases" "mouse" "+"))
If someone is rough then they chase the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "mouse" "+"))
If someone chases the cat then the cat eats the mouse.
((("someone" "chases" "cat" "+")) -> ("cat" "eats" "mouse" "+"))
If someone is red and they do not chase the mouse then the mouse does not eat the cat.
((("someone" "is" "red" "+") ("someone" "chases" "mouse" "~")) -> ("mouse" "eats" "cat" "-"))
The mouse eats the cat.
True
1
proof
[(triple4)]
("mouse" "eats" "cat" "+")
triple4
The cat is not rough.
False
1
inv-proof
[(triple2)]
("cat" "is" "rough" "-")
triple2
The cat eats the mouse.
True
2
proof
[(((triple3) -> rule5))]
("cat" "eats" "mouse" "+")
((triple3) -> (rule5 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat does not eat the mouse.
False
2
inv-proof
[(((triple3) -> rule5))]
("cat" "eats" "mouse" "-")
((triple3) -> (rule5 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("mouse" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int2
The mouse is not rough.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule1))]
("mouse" "is" "rough" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int2
The mouse chases the mouse.
True
4
proof
[(((((((triple3) -> rule5)) -> rule1)) -> rule4))]
("mouse" "chases" "mouse" "+")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int3
The mouse does not chase the mouse.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule1)) -> rule4))]
("mouse" "chases" "mouse" "-")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int3
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "green" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The cat does not need the mouse.
Unknown
inv-random
[@0: The cat needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "mouse" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The cat is red.[(triple1)] The cat is rough.[(triple2)] The mouse chases the cat.[(triple3)] The mouse eats the cat.[(triple4)] The mouse is not green.[(triple5)] The mouse is not nice.[(triple6)] The mouse needs the cat.[(triple7)] @1: The cat chases the mouse.[(((triple2) -> rule4))] The cat eats the mouse.[(((triple3) -> rule5))] @2: The mouse is rough.[(((((triple3) -> rule5)) -> rule1))] @3: The mouse chases the mouse.[(((((((triple3) -> rule5)) -> rule1)) -> rule4))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple3
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple4
The mouse is not green.
("mouse" "is" "green" "-")
triple5
The mouse is not nice.
("mouse" "is" "nice" "-")
triple6
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple7
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple2) -> (rule4 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
((triple3) -> (rule5 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int3