The dog needs the rabbit. The lion is young. The rabbit needs the lion. If something needs the lion and it is young then the lion chases the rabbit. If something is cold then it eats the dog. If something chases the lion then it is blue. All blue things are young. If something is cold then it needs the lion. If the rabbit needs the lion then the rabbit chases the lion.
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The lion is young.
("lion" "is" "young" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If something needs the lion and it is young then the lion chases the rabbit.
((("something" "needs" "lion" "+") ("something" "is" "young" "+")) -> ("lion" "chases" "rabbit" "+"))
If something is cold then it eats the dog.
((("something" "is" "cold" "+")) -> ("something" "eats" "dog" "+"))
If something chases the lion then it is blue.
((("something" "chases" "lion" "+")) -> ("something" "is" "blue" "+"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is cold then it needs the lion.
((("something" "is" "cold" "+")) -> ("something" "needs" "lion" "+"))
If the rabbit needs the lion then the rabbit chases the lion.
((("rabbit" "needs" "lion" "+")) -> ("rabbit" "chases" "lion" "+"))
The dog needs the rabbit.
True
1
proof
[(triple1)]
("dog" "needs" "rabbit" "+")
triple1
The dog does not need the rabbit.
False
1
inv-proof
[(triple1)]
("dog" "needs" "rabbit" "-")
triple1
The rabbit chases the lion.
True
2
proof
[(((triple3) -> rule6))]
("rabbit" "chases" "lion" "+")
((triple3) -> (rule6 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit does not chase the lion.
False
2
inv-proof
[(((triple3) -> rule6))]
("rabbit" "chases" "lion" "-")
((triple3) -> (rule6 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit is blue.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("rabbit" "is" "blue" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The rabbit is not blue.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule3))]
("rabbit" "is" "blue" "-")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The rabbit is young.
True
4
proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule4))]
("rabbit" "is" "young" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int3
The rabbit is not young.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule4))]
("rabbit" "is" "young" "-")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int3
The dog is not young.
Unknown
inv-rconc
[@2: The dog is young.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("dog" "is" "young" "-")
The dog eats the dog.
Unknown
rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "dog" "+")
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "blue" "-")
The lion is blue.
Unknown
rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "blue" "+")
The rabbit does not chase the dog.
Unknown
inv-random
[@0: The rabbit chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "dog" "-")
The lion needs the dog.
Unknown
random
[@0: The lion needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "dog" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The dog chases the lion.
Unknown
random
[@0: The dog chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "lion" "+")
@0: The dog needs the rabbit.[(triple1)] The lion is young.[(triple2)] The rabbit needs the lion.[(triple3)] @1: The rabbit chases the lion.[(((triple3) -> rule6))] @2: The rabbit is blue.[(((((triple3) -> rule6)) -> rule3))] @3: The rabbit is young.[(((((((triple3) -> rule6)) -> rule3)) -> rule4))] @4: The lion chases the rabbit.[(((triple3 ((((((triple3) -> rule6)) -> rule3)) -> rule4)) -> rule1))]
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple3
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
((triple3) -> (rule6 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((triple3 ((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int4