The cow does not chase the lion. The cow is red. The cow needs the lion. The cow does not visit the lion. The cow visits the rabbit. The lion chases the rabbit. The rabbit does not chase the lion. The rabbit is not round. The rabbit is young. The rabbit needs the cow. The rabbit does not visit the cow. The rabbit visits the lion. If something is young and red then it does not need the lion. If something needs the rabbit and it needs the lion then it needs the cow. All round things are red. If something needs the lion then the lion visits the rabbit. If the cow chases the lion then the lion does not chase the rabbit. If something visits the lion and the lion visits the rabbit then the rabbit does not need the lion.
The cow does not chase the lion.
("cow" "chases" "lion" "-")
The cow is red.
("cow" "is" "red" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow does not visit the lion.
("cow" "visits" "lion" "-")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit does not visit the cow.
("rabbit" "visits" "cow" "-")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something is young and red then it does not need the lion.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "needs" "lion" "-"))
If something needs the rabbit and it needs the lion then it needs the cow.
((("something" "needs" "rabbit" "+") ("something" "needs" "lion" "+")) -> ("something" "needs" "cow" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something needs the lion then the lion visits the rabbit.
((("something" "needs" "lion" "+")) -> ("lion" "visits" "rabbit" "+"))
If the cow chases the lion then the lion does not chase the rabbit.
((("cow" "chases" "lion" "+")) -> ("lion" "chases" "rabbit" "-"))
If something visits the lion and the lion visits the rabbit then the rabbit does not need the lion.
((("something" "visits" "lion" "+") ("lion" "visits" "rabbit" "+")) -> ("rabbit" "needs" "lion" "-"))
The rabbit does not chase the lion.
True
1
proof
[(triple7)]
("rabbit" "chases" "lion" "-")
triple7
The cow is not red.
False
1
inv-proof
[(triple2)]
("cow" "is" "red" "-")
triple2
The lion visits the rabbit.
True
2
proof
[(((triple3) -> rule4))]
("lion" "visits" "rabbit" "+")
((triple3) -> (rule4 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion does not visit the rabbit.
False
2
inv-proof
[(((triple3) -> rule4))]
("lion" "visits" "rabbit" "-")
((triple3) -> (rule4 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The rabbit does not need the lion.
True
4
proof
[(((triple12 ((triple3) -> rule4)) -> rule6))]
("rabbit" "needs" "lion" "-")
((triple12 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The rabbit needs the lion.
False
4
inv-proof
[(((triple12 ((triple3) -> rule4)) -> rule6))]
("rabbit" "needs" "lion" "+")
((triple12 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "red" "-")
The cow needs the cow.
Unknown
rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "cow" "+")
The lion does not need the cow.
Unknown
inv-rconc
[@1: The lion needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "cow" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The cow does not chase the rabbit.
Unknown
inv-random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The cow does not chase the lion.[(triple1)] The cow does not visit the lion.[(triple4)] The cow is red.[(triple2)] The cow needs the lion.[(triple3)] The cow visits the rabbit.[(triple5)] The lion chases the rabbit.[(triple6)] The rabbit does not chase the lion.[(triple7)] The rabbit does not visit the cow.[(triple11)] The rabbit is not round.[(triple8)] The rabbit is young.[(triple9)] The rabbit needs the cow.[(triple10)] The rabbit visits the lion.[(triple12)] @1: The lion visits the rabbit.[(((triple3) -> rule4))] @2: The rabbit does not need the lion.[(((triple12 ((triple3) -> rule4)) -> rule6))]
The cow does not chase the lion.
("cow" "chases" "lion" "-")
triple1
The cow does not visit the lion.
("cow" "visits" "lion" "-")
triple4
The cow is red.
("cow" "is" "red" "+")
triple2
The cow needs the lion.
("cow" "needs" "lion" "+")
triple3
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple5
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple6
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
triple7
The rabbit does not visit the cow.
("rabbit" "visits" "cow" "-")
triple11
The rabbit is not round.
("rabbit" "is" "round" "-")
triple8
The rabbit is young.
("rabbit" "is" "young" "+")
triple9
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple10
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple12
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
((triple3) -> (rule4 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
((triple12 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2