The bear is nice. The cat eats the bear. The mouse is young. Nice things are young. If something eats the bear then the bear likes the mouse. If something likes the mouse then the mouse does not eat the bear. If the mouse is cold and the mouse is rough then the mouse does not eat the bear. If the mouse eats the bear and the bear needs the cat then the cat eats the mouse. If the bear is young and the mouse does not eat the bear then the bear is rough.
The bear is nice.
("bear" "is" "nice" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The mouse is young.
("mouse" "is" "young" "+")
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something eats the bear then the bear likes the mouse.
((("something" "eats" "bear" "+")) -> ("bear" "likes" "mouse" "+"))
If something likes the mouse then the mouse does not eat the bear.
((("something" "likes" "mouse" "+")) -> ("mouse" "eats" "bear" "-"))
If the mouse is cold and the mouse is rough then the mouse does not eat the bear.
((("mouse" "is" "cold" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "eats" "bear" "-"))
If the mouse eats the bear and the bear needs the cat then the cat eats the mouse.
((("mouse" "eats" "bear" "+") ("bear" "needs" "cat" "+")) -> ("cat" "eats" "mouse" "+"))
If the bear is young and the mouse does not eat the bear then the bear is rough.
((("bear" "is" "young" "+") ("mouse" "eats" "bear" "~")) -> ("bear" "is" "rough" "+"))
The cat eats the bear.
True
1
proof
[(triple2)]
("cat" "eats" "bear" "+")
triple2
The mouse is not young.
False
1
inv-proof
[(triple3)]
("mouse" "is" "young" "-")
triple3
The bear is young.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "young" "+")
((triple1) -> (rule1 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "young" "-")
((triple1) -> (rule1 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The mouse does not eat the bear.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("mouse" "eats" "bear" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse eats the bear.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("mouse" "eats" "bear" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The bear is rough.
True
6
proof
[(((((triple1) -> rule1) ((((triple2) -> rule2)) -> rule3)) -> rule6))]
("bear" "is" "rough" "+")
((((triple1) -> (rule1 % int4)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The bear is young.
("bear" "is" "young" "+")
int4
The bear is not rough.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple2) -> rule2)) -> rule3)) -> rule6))]
("bear" "is" "rough" "-")
((((triple1) -> (rule1 % int4)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The bear is young.
("bear" "is" "young" "+")
int4
The cat does not eat the mouse.
Unknown
inv-rconc
[@1: The cat eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "mouse" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "young" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The bear likes the cat.
Unknown
random
[@0: The bear likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cat" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The mouse needs the bear.
Unknown
random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "+")
@0: The bear is nice.[(triple1)] The cat eats the bear.[(triple2)] The mouse is young.[(triple3)] @1: The bear is young.[(((triple1) -> rule1))] The bear likes the mouse.[(((triple2) -> rule2))] @2: The mouse does not eat the bear.[(((((triple2) -> rule2)) -> rule3))] @3: The bear is rough.[(((((triple1) -> rule1) ((((triple2) -> rule2)) -> rule3)) -> rule6))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cat eats the bear.
("cat" "eats" "bear" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule1 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((triple2) -> (rule2 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
((((triple1) -> (rule1 % int4)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The bear is young.
("bear" "is" "young" "+")
int4