The dog is cold. The dog is kind. The dog is round. The dog sees the mouse. The lion needs the mouse. The lion sees the dog. The lion sees the mouse. The lion visits the dog. The lion visits the mouse. The mouse is red. The mouse sees the dog. The mouse visits the lion. If something sees the mouse then the mouse visits the lion. If something is young and round then it sees the lion. If something sees the mouse then the mouse is round.
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is round.
("dog" "is" "round" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If something sees the mouse then the mouse visits the lion.
((("something" "sees" "mouse" "+")) -> ("mouse" "visits" "lion" "+"))
If something is young and round then it sees the lion.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "sees" "lion" "+"))
If something sees the mouse then the mouse is round.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "round" "+"))
The mouse visits the lion.
True
1
proof
[(triple12 OR ((triple4) -> rule1) OR ((triple7) -> rule1))]
("mouse" "visits" "lion" "+")
triple12
((triple4) -> (rule1 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
((triple7) -> (rule1 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The lion does not need the mouse.
False
1
inv-proof
[(triple5)]
("lion" "needs" "mouse" "-")
triple5
The mouse is round.
True
2
proof
[(((triple4) -> rule3) OR ((triple7) -> rule3))]
("mouse" "is" "round" "+")
((triple4) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple7) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
2
inv-proof
[(((triple4) -> rule3) OR ((triple7) -> rule3))]
("mouse" "is" "round" "-")
((triple4) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple7) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The dog does not see the lion.
Unknown
inv-rconc
[@1: The dog sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "lion" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "lion" "+")
The mouse does not need the dog.
Unknown
inv-random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The dog is cold.[(triple1)] The dog is kind.[(triple2)] The dog is round.[(triple3)] The dog sees the mouse.[(triple4)] The lion needs the mouse.[(triple5)] The lion sees the dog.[(triple6)] The lion sees the mouse.[(triple7)] The lion visits the dog.[(triple8)] The lion visits the mouse.[(triple9)] The mouse is red.[(triple10)] The mouse sees the dog.[(triple11)] The mouse visits the lion.[(triple12 OR ((triple4) -> rule1) OR ((triple7) -> rule1))] @1: The mouse is round.[(((triple4) -> rule3) OR ((triple7) -> rule3))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple4
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple5
The lion sees the dog.
("lion" "sees" "dog" "+")
triple6
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple7
The lion visits the dog.
("lion" "visits" "dog" "+")
triple8
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple9
The mouse is red.
("mouse" "is" "red" "+")
triple10
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple11
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple12
((triple4) -> (rule1 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
((triple7) -> (rule1 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple4) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple7) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1