The cow is round. The cow is not young. The cow likes the mouse. The cow likes the rabbit. The cow does not see the mouse. The cow sees the rabbit. The mouse eats the cow. The mouse is cold. The mouse is red. The mouse is not young. The mouse does not like the cow. The mouse likes the rabbit. The mouse sees the cow. The rabbit likes the mouse. The rabbit does not see the cow. If something is cold then it eats the mouse. If something is rough and red then it sees the rabbit. If something eats the mouse then it is rough. If something likes the cow then the cow sees the rabbit. Rough, young things are round. If the cow does not eat the mouse and the cow does not see the rabbit then the mouse is round.
The cow is round.
("cow" "is" "round" "+")
The cow is not young.
("cow" "is" "young" "-")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse does not like the cow.
("mouse" "likes" "cow" "-")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit does not see the cow.
("rabbit" "sees" "cow" "-")
If something is cold then it eats the mouse.
((("something" "is" "cold" "+")) -> ("something" "eats" "mouse" "+"))
If something is rough and red then it sees the rabbit.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "sees" "rabbit" "+"))
If something eats the mouse then it is rough.
((("something" "eats" "mouse" "+")) -> ("something" "is" "rough" "+"))
If something likes the cow then the cow sees the rabbit.
((("something" "likes" "cow" "+")) -> ("cow" "sees" "rabbit" "+"))
Rough, young things are round.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If the cow does not eat the mouse and the cow does not see the rabbit then the mouse is round.
((("cow" "eats" "mouse" "~") ("cow" "sees" "rabbit" "~")) -> ("mouse" "is" "round" "+"))
The mouse is not young.
True
1
proof
[(triple10)]
("mouse" "is" "young" "-")
triple10
The mouse is not cold.
False
1
inv-proof
[(triple8)]
("mouse" "is" "cold" "-")
triple8
The mouse eats the mouse.
True
2
proof
[(((triple8) -> rule1))]
("mouse" "eats" "mouse" "+")
((triple8) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse does not eat the mouse.
False
2
inv-proof
[(((triple8) -> rule1))]
("mouse" "eats" "mouse" "-")
((triple8) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple8) -> rule1)) -> rule3))]
("mouse" "is" "rough" "+")
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse is not rough.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule3))]
("mouse" "is" "rough" "-")
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse sees the rabbit.
True
5
proof
[(((((((triple8) -> rule1)) -> rule3) triple9) -> rule2))]
("mouse" "sees" "rabbit" "+")
((((((triple8) -> (rule1 % int3))) -> (rule3 % int2)) triple9) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
The mouse does not see the rabbit.
False
5
inv-proof
[(((((((triple8) -> rule1)) -> rule3) triple9) -> rule2))]
("mouse" "sees" "rabbit" "-")
((((((triple8) -> (rule1 % int3))) -> (rule3 % int2)) triple9) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
The cow is not rough.
Unknown
inv-rconc
[@2: The cow is rough.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("cow" "is" "rough" "-")
The rabbit is round.
Unknown
rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "round" "+")
The cow does not eat the mouse.
Unknown
inv-rconc
[@1: The cow eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "mouse" "-")
The rabbit eats the mouse.
Unknown
rconc
[@1: The rabbit eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "mouse" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The rabbit does not like the cow.
Unknown
inv-random
[@0: The rabbit likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cow" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The cow does not see the mouse.[(triple5)] The cow is not young.[(triple2)] The cow is round.[(triple1)] The cow likes the mouse.[(triple3)] The cow likes the rabbit.[(triple4)] The cow sees the rabbit.[(triple6)] The mouse does not like the cow.[(triple11)] The mouse eats the cow.[(triple7)] The mouse is cold.[(triple8)] The mouse is not young.[(triple10)] The mouse is red.[(triple9)] The mouse likes the rabbit.[(triple12)] The mouse sees the cow.[(triple13)] The rabbit does not see the cow.[(triple15)] The rabbit likes the mouse.[(triple14)] @1: The mouse eats the mouse.[(((triple8) -> rule1))] @2: The mouse is rough.[(((((triple8) -> rule1)) -> rule3))] @3: The mouse sees the rabbit.[(((((((triple8) -> rule1)) -> rule3) triple9) -> rule2))]
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
triple5
The cow is not young.
("cow" "is" "young" "-")
triple2
The cow is round.
("cow" "is" "round" "+")
triple1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple3
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple4
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple6
The mouse does not like the cow.
("mouse" "likes" "cow" "-")
triple11
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse is not young.
("mouse" "is" "young" "-")
triple10
The mouse is red.
("mouse" "is" "red" "+")
triple9
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple12
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple13
The rabbit does not see the cow.
("rabbit" "sees" "cow" "-")
triple15
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple14
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple8) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
((((((triple8) -> (rule1 % int3))) -> (rule3 % int2)) triple9) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3