The dog is cold. The dog is round. The dog needs the lion. The dog needs the mouse. The dog sees the lion. The dog sees the mouse. The dog visits the lion. The lion is blue. The lion is round. The lion needs the dog. The lion needs the mouse. The lion sees the mouse. The lion visits the dog. The mouse is cold. The mouse is red. If someone visits the lion then the lion sees the dog. If someone is blue and round then they need the lion. If someone needs the dog then the dog needs the lion. If someone needs the mouse and they visit the mouse then they are young. If someone is young then they need the mouse. If someone is blue then they visit the lion. If someone is young and they visit the mouse then they need the lion. If someone needs the mouse and they are round then the mouse visits the lion.
The dog is cold.
("dog" "is" "cold" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
If someone visits the lion then the lion sees the dog.
((("someone" "visits" "lion" "+")) -> ("lion" "sees" "dog" "+"))
If someone is blue and round then they need the lion.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the dog then the dog needs the lion.
((("someone" "needs" "dog" "+")) -> ("dog" "needs" "lion" "+"))
If someone needs the mouse and they visit the mouse then they are young.
((("someone" "needs" "mouse" "+") ("someone" "visits" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they need the mouse.
((("someone" "is" "young" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is blue then they visit the lion.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "lion" "+"))
If someone is young and they visit the mouse then they need the lion.
((("someone" "is" "young" "+") ("someone" "visits" "mouse" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the mouse and they are round then the mouse visits the lion.
((("someone" "needs" "mouse" "+") ("someone" "is" "round" "+")) -> ("mouse" "visits" "lion" "+"))
The dog needs the mouse.
True
1
proof
[(triple4)]
("dog" "needs" "mouse" "+")
triple4
The dog does not need the mouse.
False
1
inv-proof
[(triple4)]
("dog" "needs" "mouse" "-")
triple4
The lion needs the lion.
True
3
proof
[(((triple8 triple9) -> rule2))]
("lion" "needs" "lion" "+")
((triple8 triple9) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple8) -> rule6))]
("lion" "visits" "lion" "-")
((triple8) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "young" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "young" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The dog is cold.[(triple1)] The dog is round.[(triple2)] The dog needs the lion.[(triple3 OR ((triple10) -> rule3))] The dog needs the mouse.[(triple4)] The dog sees the lion.[(triple5)] The dog sees the mouse.[(triple6)] The dog visits the lion.[(triple7)] The lion is blue.[(triple8)] The lion is round.[(triple9)] The lion needs the dog.[(triple10)] The lion needs the mouse.[(triple11)] The lion sees the mouse.[(triple12)] The lion visits the dog.[(triple13)] The mouse is cold.[(triple14)] The mouse is red.[(triple15)] @1: The lion needs the lion.[(((triple8 triple9) -> rule2))] The lion sees the dog.[(((triple7) -> rule1) OR ((((triple8) -> rule6)) -> rule1) OR ((((triple11 triple9) -> rule8)) -> rule1) OR ((((triple4 triple2) -> rule8)) -> rule1))] The lion visits the lion.[(((triple8) -> rule6))] The mouse visits the lion.[(((triple11 triple9) -> rule8) OR ((triple4 triple2) -> rule8))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The dog needs the lion.
("dog" "needs" "lion" "+")
triple3
((triple10) -> (rule3 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple4
The dog sees the lion.
("dog" "sees" "lion" "+")
triple5
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple6
The dog visits the lion.
("dog" "visits" "lion" "+")
triple7
The lion is blue.
("lion" "is" "blue" "+")
triple8
The lion is round.
("lion" "is" "round" "+")
triple9
The lion needs the dog.
("lion" "needs" "dog" "+")
triple10
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple11
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple12
The lion visits the dog.
("lion" "visits" "dog" "+")
triple13
The mouse is cold.
("mouse" "is" "cold" "+")
triple14
The mouse is red.
("mouse" "is" "red" "+")
triple15
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple8 triple9) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
((triple7) -> (rule1 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
((((triple11 triple9) -> (rule8 % int2))) -> (rule1 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int2
((((triple4 triple2) -> (rule8 % int2))) -> (rule1 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple8) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
((triple11 triple9) -> (rule8 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
((triple4 triple2) -> (rule8 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1