The dog needs the rabbit. The dog sees the rabbit. The dog visits the lion. The dog does not visit the rabbit. The lion needs the dog. The rabbit is cold. The rabbit is kind. The rabbit is red. The rabbit needs the dog. The rabbit needs the lion. If something needs the dog then the dog sees the lion. If something visits the dog then the dog sees the lion. If something needs the rabbit and it is red then the rabbit visits the lion. If something is cold and it sees the lion then it is rough. If something is cold and it does not need the rabbit then it sees the lion. If something sees the lion then it is red.
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
The lion needs the dog.
("lion" "needs" "dog" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If something needs the dog then the dog sees the lion.
((("something" "needs" "dog" "+")) -> ("dog" "sees" "lion" "+"))
If something visits the dog then the dog sees the lion.
((("something" "visits" "dog" "+")) -> ("dog" "sees" "lion" "+"))
If something needs the rabbit and it is red then the rabbit visits the lion.
((("something" "needs" "rabbit" "+") ("something" "is" "red" "+")) -> ("rabbit" "visits" "lion" "+"))
If something is cold and it sees the lion then it is rough.
((("something" "is" "cold" "+") ("something" "sees" "lion" "+")) -> ("something" "is" "rough" "+"))
If something is cold and it does not need the rabbit then it sees the lion.
((("something" "is" "cold" "+") ("something" "needs" "rabbit" "~")) -> ("something" "sees" "lion" "+"))
If something sees the lion then it is red.
((("something" "sees" "lion" "+")) -> ("something" "is" "red" "+"))
The rabbit is cold.
True
1
proof
[(triple6)]
("rabbit" "is" "cold" "+")
triple6
The rabbit does not need the dog.
False
1
inv-proof
[(triple9)]
("rabbit" "needs" "dog" "-")
triple9
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "rough" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The dog does not visit the rabbit.[(triple4)] The dog needs the rabbit.[(triple1)] The dog sees the rabbit.[(triple2)] The dog visits the lion.[(triple3)] The lion needs the dog.[(triple5)] The rabbit is cold.[(triple6)] The rabbit is kind.[(triple7)] The rabbit is red.[(triple8)] The rabbit needs the dog.[(triple9)] The rabbit needs the lion.[(triple10)] @1: The dog sees the lion.[(((triple5) -> rule1) OR ((triple9) -> rule1))] @2: The dog is red.[(((((triple5) -> rule1)) -> rule6) OR ((((triple9) -> rule1)) -> rule6))] @3: The rabbit visits the lion.[(((triple1 ((((triple5) -> rule1)) -> rule6)) -> rule3) OR ((triple1 ((((triple9) -> rule1)) -> rule6)) -> rule3))]
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
triple4
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple2
The dog visits the lion.
("dog" "visits" "lion" "+")
triple3
The lion needs the dog.
("lion" "needs" "dog" "+")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple8
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple9
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple10
The dog sees the lion.
("dog" "sees" "lion" "+")
((triple5) -> (rule1 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
((triple9) -> (rule1 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
((triple1 ((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
((triple1 ((((triple9) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3