The cow is young. The cow needs the rabbit. The lion eats the rabbit. The lion is cold. The lion visits the rabbit. The rabbit eats the cow. The rabbit is nice. If someone is young and big then they need the rabbit. If someone visits the lion and they need the rabbit then the rabbit eats the cow. If the cow is young then the cow eats the rabbit. If someone is rough then they need the rabbit. If the cow eats the rabbit then the rabbit is rough. If someone is nice then they eat the lion.
The cow is young.
("cow" "is" "young" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
If someone is young and big then they need the rabbit.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone visits the lion and they need the rabbit then the rabbit eats the cow.
((("someone" "visits" "lion" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "eats" "cow" "+"))
If the cow is young then the cow eats the rabbit.
((("cow" "is" "young" "+")) -> ("cow" "eats" "rabbit" "+"))
If someone is rough then they need the rabbit.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "rabbit" "+"))
If the cow eats the rabbit then the rabbit is rough.
((("cow" "eats" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If someone is nice then they eat the lion.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "lion" "+"))
The lion is cold.
True
1
proof
[(triple4)]
("lion" "is" "cold" "+")
triple4
The lion does not visit the rabbit.
False
1
inv-proof
[(triple5)]
("lion" "visits" "rabbit" "-")
triple5
The rabbit eats the lion.
True
2
proof
[(((triple7) -> rule6))]
("rabbit" "eats" "lion" "+")
((triple7) -> (rule6 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The cow does not eat the rabbit.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "eats" "rabbit" "-")
((triple1) -> (rule3 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The rabbit is rough.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("rabbit" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The rabbit is not rough.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("rabbit" "is" "rough" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The rabbit needs the rabbit.
True
4
proof
[(((((((triple1) -> rule3)) -> rule5)) -> rule4))]
("rabbit" "needs" "rabbit" "+")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The rabbit does not need the rabbit.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule5)) -> rule4))]
("rabbit" "needs" "rabbit" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "lion" "-")
The cow eats the lion.
Unknown
rconc
[@1: The cow eats the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "eats" "lion" "+")
The lion does not need the rabbit.
Unknown
inv-rconc
[@1: The lion needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "rabbit" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The lion does not visit the cow.
Unknown
inv-random
[@0: The lion visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cow" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow is young.[(triple1)] The cow needs the rabbit.[(triple2)] The lion eats the rabbit.[(triple3)] The lion is cold.[(triple4)] The lion visits the rabbit.[(triple5)] The rabbit eats the cow.[(triple6)] The rabbit is nice.[(triple7)] @1: The cow eats the rabbit.[(((triple1) -> rule3))] The rabbit eats the lion.[(((triple7) -> rule6))] @2: The rabbit is rough.[(((((triple1) -> rule3)) -> rule5))] @3: The rabbit needs the rabbit.[(((((((triple1) -> rule3)) -> rule5)) -> rule4))]
The cow is young.
("cow" "is" "young" "+")
triple1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple5
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((triple1) -> (rule3 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
((triple7) -> (rule6 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3