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