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