The dog eats the mouse. The dog eats the rabbit. The dog is young. The lion needs the rabbit. The mouse chases the rabbit. The rabbit is kind. The rabbit needs the dog. Rough things are young. If something needs the dog then it is rough.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is young.
("dog" "is" "young" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something needs the dog then it is rough.
((("something" "needs" "dog" "+")) -> ("something" "is" "rough" "+"))
The dog eats the mouse.
True
1
proof
[(triple1)]
("dog" "eats" "mouse" "+")
triple1
The dog does not eat the mouse.
False
1
inv-proof
[(triple1)]
("dog" "eats" "mouse" "-")
triple1
The rabbit is rough.
True
2
proof
[(((triple7) -> rule2))]
("rabbit" "is" "rough" "+")
((triple7) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is not rough.
False
2
inv-proof
[(((triple7) -> rule2))]
("rabbit" "is" "rough" "-")
((triple7) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is young.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("rabbit" "is" "young" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is not young.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("rabbit" "is" "young" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "rough" "-")
The mouse is young.
Unknown
rconc
[@2: The mouse is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("mouse" "is" "young" "+")
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "rough" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The rabbit does not chase the lion.
Unknown
inv-random
[@0: The rabbit chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "lion" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
@0: The dog eats the mouse.[(triple1)] The dog eats the rabbit.[(triple2)] The dog is young.[(triple3)] The lion needs the rabbit.[(triple4)] The mouse chases the rabbit.[(triple5)] The rabbit is kind.[(triple6)] The rabbit needs the dog.[(triple7)] @1: The rabbit is rough.[(((triple7) -> rule2))] @2: The rabbit is young.[(((((triple7) -> rule2)) -> rule1))]
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple4
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple5
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple6
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple7) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2