The dog is kind. The lion sees the mouse. The mouse sees the rabbit. The rabbit eats the mouse. If something is young and it eats the rabbit then the rabbit sees the lion. If the rabbit sees the mouse then the rabbit chases the mouse. If something eats the mouse then it sees the mouse. If something eats the lion then the lion sees the mouse. If something sees the dog and the dog chases the mouse then it chases the dog. If something chases the mouse then it sees the dog.
The dog is kind.
("dog" "is" "kind" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
If something is young and it eats the rabbit then the rabbit sees the lion.
((("something" "is" "young" "+") ("something" "eats" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
If the rabbit sees the mouse then the rabbit chases the mouse.
((("rabbit" "sees" "mouse" "+")) -> ("rabbit" "chases" "mouse" "+"))
If something eats the mouse then it sees the mouse.
((("something" "eats" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
If something eats the lion then the lion sees the mouse.
((("something" "eats" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If something sees the dog and the dog chases the mouse then it chases the dog.
((("something" "sees" "dog" "+") ("dog" "chases" "mouse" "+")) -> ("something" "chases" "dog" "+"))
If something chases the mouse then it sees the dog.
((("something" "chases" "mouse" "+")) -> ("something" "sees" "dog" "+"))
The dog is kind.
True
1
proof
[(triple1)]
("dog" "is" "kind" "+")
triple1
The lion does not see the mouse.
False
1
inv-proof
[(triple2)]
("lion" "sees" "mouse" "-")
triple2
The rabbit sees the mouse.
True
2
proof
[(((triple4) -> rule3))]
("rabbit" "sees" "mouse" "+")
((triple4) -> (rule3 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit does not see the mouse.
False
2
inv-proof
[(((triple4) -> rule3))]
("rabbit" "sees" "mouse" "-")
((triple4) -> (rule3 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit chases the mouse.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("rabbit" "chases" "mouse" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit does not chase the mouse.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("rabbit" "chases" "mouse" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit does not see the lion.
Unknown
inv-rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "lion" "-")
The rabbit chases the dog.
Unknown
rconc
[@1: The rabbit chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "chases" "dog" "+")
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse eats the dog.
Unknown
random
[@0: The mouse eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "dog" "+")
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 lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The dog is kind.[(triple1)] The lion sees the mouse.[(triple2)] The mouse sees the rabbit.[(triple3)] The rabbit eats the mouse.[(triple4)] @1: The rabbit sees the mouse.[(((triple4) -> rule3))] @2: The rabbit chases the mouse.[(((((triple4) -> rule3)) -> rule2))] @3: The rabbit sees the dog.[(((((((triple4) -> rule3)) -> rule2)) -> rule6))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple3
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple4
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((triple4) -> (rule3 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int3