The cow sees the rabbit. The rabbit eats the cow. All nice, big people are rough. If someone sees the rabbit and they are big then they are nice. If the cow sees the rabbit then the cow is big.
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
All nice, big people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the rabbit and they are big then they are nice.
((("someone" "sees" "rabbit" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If the cow sees the rabbit then the cow is big.
((("cow" "sees" "rabbit" "+")) -> ("cow" "is" "big" "+"))
The rabbit eats the cow.
True
1
proof
[(triple2)]
("rabbit" "eats" "cow" "+")
triple2
The cow does not see the rabbit.
False
1
inv-proof
[(triple1)]
("cow" "sees" "rabbit" "-")
triple1
The cow is big.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "big" "+")
((triple1) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "is" "big" "-")
((triple1) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is nice.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("cow" "is" "nice" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("cow" "is" "nice" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit is nice.
Unknown
rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "nice" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The rabbit does not like the cow.
Unknown
inv-random
[@0: The rabbit likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cow" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The cow sees the rabbit.[(triple1)] The rabbit eats the cow.[(triple2)] @1: The cow is big.[(((triple1) -> rule3))] @2: The cow is nice.[(((triple1 ((triple1) -> rule3)) -> rule2))] @3: The cow is rough.[(((((triple1 ((triple1) -> rule3)) -> rule2) ((triple1) -> rule3)) -> rule1))]
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
((triple1) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3