The cow is blue. The rabbit is cold. If someone visits the rabbit then the rabbit is blue. If someone is blue then they are red. If the rabbit eats the cow then the rabbit visits the cow. If someone is cold then they visit the rabbit. If someone is cold and they eat the rabbit then they chase the cow. If the rabbit is not blue then the rabbit is not young.
The cow is blue.
("cow" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
If someone visits the rabbit then the rabbit is blue.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If the rabbit eats the cow then the rabbit visits the cow.
((("rabbit" "eats" "cow" "+")) -> ("rabbit" "visits" "cow" "+"))
If someone is cold then they visit the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is cold and they eat the rabbit then they chase the cow.
((("someone" "is" "cold" "+") ("someone" "eats" "rabbit" "+")) -> ("someone" "chases" "cow" "+"))
If the rabbit is not blue then the rabbit is not young.
((("rabbit" "is" "blue" "~")) -> ("rabbit" "is" "young" "-"))
The cow is blue.
True
1
proof
[(triple1)]
("cow" "is" "blue" "+")
triple1
The cow is not blue.
False
1
inv-proof
[(triple1)]
("cow" "is" "blue" "-")
triple1
The cow is red.
True
2
proof
[(((triple1) -> rule2))]
("cow" "is" "red" "+")
((triple1) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The rabbit does not visit the rabbit.
False
2
inv-proof
[(((triple2) -> rule4))]
("rabbit" "visits" "rabbit" "-")
((triple2) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is blue.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("rabbit" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is not blue.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("rabbit" "is" "blue" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is red.
True
4
proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule2))]
("rabbit" "is" "red" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit is not red.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule2))]
("rabbit" "is" "red" "-")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The cow does not visit the rabbit.
Unknown
inv-rconc
[@1: The cow visits the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "visits" "rabbit" "-")
The rabbit visits the cow.
Unknown
rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "cow" "+")
The rabbit does not chase the cow.
Unknown
inv-rconc
[@1: The rabbit chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "chases" "cow" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "cow" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow is blue.[(triple1)] The rabbit is cold.[(triple2)] @1: The cow is red.[(((triple1) -> rule2))] The rabbit visits the rabbit.[(((triple2) -> rule4))] @2: The rabbit is blue.[(((((triple2) -> rule4)) -> rule1))] @3: The rabbit is red.[(((((((triple2) -> rule4)) -> rule1)) -> rule2))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
((triple1) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple2) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3