The cow is cold. The cow is not green. The cow is round. The cow likes the rabbit. The cow does not see the rabbit. The cow visits the rabbit. The rabbit is not cold. The rabbit likes the cow. The rabbit sees the cow. The rabbit visits the cow. If someone is cold then they like the cow. If someone visits the cow then they are young. If someone is young then they see the rabbit. If someone is big and they do not like the rabbit then they are green. If someone likes the cow then the cow does not see the rabbit. If the cow visits the rabbit then the cow is not young.
The cow is cold.
("cow" "is" "cold" "+")
The cow is not green.
("cow" "is" "green" "-")
The cow is round.
("cow" "is" "round" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If someone is cold then they like the cow.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "cow" "+"))
If someone visits the cow then they are young.
((("someone" "visits" "cow" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they see the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is big and they do not like the rabbit then they are green.
((("someone" "is" "big" "+") ("someone" "likes" "rabbit" "~")) -> ("someone" "is" "green" "+"))
If someone likes the cow then the cow does not see the rabbit.
((("someone" "likes" "cow" "+")) -> ("cow" "sees" "rabbit" "-"))
If the cow visits the rabbit then the cow is not young.
((("cow" "visits" "rabbit" "+")) -> ("cow" "is" "young" "-"))
The rabbit visits the cow.
True
1
proof
[(triple10)]
("rabbit" "visits" "cow" "+")
triple10
The rabbit does not see the cow.
False
1
inv-proof
[(triple9)]
("rabbit" "sees" "cow" "-")
triple9
The rabbit is young.
True
2
proof
[(((triple10) -> rule2))]
("rabbit" "is" "young" "+")
((triple10) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is not young.
False
2
inv-proof
[(((triple10) -> rule2))]
("rabbit" "is" "young" "-")
((triple10) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit sees the rabbit.
True
3
proof
[(((((triple10) -> rule2)) -> rule3))]
("rabbit" "sees" "rabbit" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit does not see the rabbit.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule3))]
("rabbit" "sees" "rabbit" "-")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "green" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
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 big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The cow does not see the rabbit.[(triple5 OR ((triple8) -> rule5) OR ((((triple1) -> rule1)) -> rule5))] The cow is cold.[(triple1)] The cow is not green.[(triple2)] The cow is round.[(triple3)] The cow likes the rabbit.[(triple4)] The cow visits the rabbit.[(triple6)] The rabbit is not cold.[(triple7)] The rabbit likes the cow.[(triple8)] The rabbit sees the cow.[(triple9)] The rabbit visits the cow.[(triple10)] @1: The cow is not young.[(((triple6) -> rule6))] The cow likes the cow.[(((triple1) -> rule1))] The rabbit is young.[(((triple10) -> rule2))] @2: The rabbit sees the rabbit.[(((((triple10) -> rule2)) -> rule3))]
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
triple5
((triple8) -> (rule5 % int1))
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is not green.
("cow" "is" "green" "-")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple4
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple6
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple7
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple8
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple9
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple10
The cow is not young.
("cow" "is" "young" "-")
((triple6) -> (rule6 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple1) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple10) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2