The rabbit is cold. The rabbit is green. The rabbit is round. If something is round then it is cold. All big, green things are not cold. Round things are cold. Round, cold things are green. If something is round and rough then it is green. All round, rough things are green. All big things are rough. If the rabbit is rough and the rabbit is round then the rabbit is green.
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All big, green things are not cold.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "-"))
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Round, cold things are green.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is round and rough then it is green.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
All round, rough things are green.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If the rabbit is rough and the rabbit is round then the rabbit is green.
((("rabbit" "is" "rough" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "is" "green" "+"))
The rabbit is cold.
True
1
proof
[(triple1 OR ((triple3) -> rule1) OR ((triple3) -> rule3))]
("rabbit" "is" "cold" "+")
triple1
((triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((triple3) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is not cold.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule1) OR ((triple3) -> rule3))]
("rabbit" "is" "cold" "-")
triple1
((triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((triple3) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The rabbit is cold.[(triple1 OR ((triple3) -> rule1) OR ((triple3) -> rule3))] The rabbit is green.[(triple2 OR ((triple3 triple1) -> rule4) OR ((triple3 ((triple3) -> rule1)) -> rule4) OR ((triple3 ((triple3) -> rule3)) -> rule4))] The rabbit is round.[(triple3)]
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple1
((triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((triple3) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
((triple3 triple1) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
triple3