The dog sees the lion. The lion is kind. The mouse eats the lion. The squirrel eats the lion. If something sees the dog then the dog is nice. If the mouse sees the dog and the dog eats the squirrel then the mouse is round. If something is kind then it sees the dog.
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
If something sees the dog then the dog is nice.
((("something" "sees" "dog" "+")) -> ("dog" "is" "nice" "+"))
If the mouse sees the dog and the dog eats the squirrel then the mouse is round.
((("mouse" "sees" "dog" "+") ("dog" "eats" "squirrel" "+")) -> ("mouse" "is" "round" "+"))
If something is kind then it sees the dog.
((("something" "is" "kind" "+")) -> ("something" "sees" "dog" "+"))
The lion is kind.
True
1
proof
[(triple2)]
("lion" "is" "kind" "+")
triple2
The squirrel does not eat the lion.
False
1
inv-proof
[(triple4)]
("squirrel" "eats" "lion" "-")
triple4
The lion sees the dog.
True
2
proof
[(((triple2) -> rule3))]
("lion" "sees" "dog" "+")
((triple2) -> (rule3 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The lion does not see the dog.
False
2
inv-proof
[(((triple2) -> rule3))]
("lion" "sees" "dog" "-")
((triple2) -> (rule3 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The dog is nice.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("dog" "is" "nice" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The dog is not nice.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("dog" "is" "nice" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "dog" "-")
The mouse sees the dog.
Unknown
rconc
[@1: The mouse sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "dog" "+")
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "round" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The squirrel does not eat the mouse.
Unknown
inv-random
[@0: The squirrel eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "mouse" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The dog sees the lion.[(triple1)] The lion is kind.[(triple2)] The mouse eats the lion.[(triple3)] The squirrel eats the lion.[(triple4)] @1: The lion sees the dog.[(((triple2) -> rule3))] @2: The dog is nice.[(((((triple2) -> rule3)) -> rule1))]
The dog sees the lion.
("dog" "sees" "lion" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple3
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple4
The lion sees the dog.
("lion" "sees" "dog" "+")
((triple2) -> (rule3 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2