Dave is furry. Dave is rough. Dave is white. Erin is big. Erin is furry. Harry is big. Harry is not cold. Harry is furry. Harry is green. Harry is rough. If Harry is green then Harry is rough. If something is rough then it is white. If something is red and green then it is white. Big things are furry. If something is big then it is furry. Cold, furry things are big. All green things are rough. Red things are not green.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Harry is green then Harry is rough.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "rough" "+"))
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If something is red and green then it is white.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Cold, furry things are big.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Red things are not green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "-"))
Erin is big.
True
1
proof
[(triple4)]
("Erin" "is" "big" "+")
triple4
Erin is not big.
False
1
inv-proof
[(triple4)]
("Erin" "is" "big" "-")
triple4
Harry is white.
True
2
proof
[(((triple10) -> rule2) OR ((((triple9) -> rule1)) -> rule2) OR ((((triple9) -> rule7)) -> rule2))]
("Harry" "is" "white" "+")
((triple10) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple9) -> (rule7 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not white.
False
2
inv-proof
[(((triple10) -> rule2) OR ((((triple9) -> rule1)) -> rule2) OR ((((triple9) -> rule7)) -> rule2))]
("Harry" "is" "white" "-")
((triple10) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple9) -> (rule7 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Erin is not white.
Unknown
inv-rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Erin" "is" "white" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Dave is furry.[(triple1)] Dave is rough.[(triple2)] Dave is white.[(triple3 OR ((triple2) -> rule2))] Erin is big.[(triple4)] Erin is furry.[(triple5 OR ((triple4) -> rule4) OR ((triple4) -> rule5))] Harry is big.[(triple6)] Harry is furry.[(triple8 OR ((triple6) -> rule4) OR ((triple6) -> rule5))] Harry is green.[(triple9)] Harry is not cold.[(triple7)] Harry is rough.[(triple10 OR ((triple9) -> rule1) OR ((triple9) -> rule7))] @1: Harry is white.[(((triple10) -> rule2) OR ((((triple9) -> rule1)) -> rule2) OR ((((triple9) -> rule7)) -> rule2))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
((triple4) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple4) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple8
((triple6) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple6) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is not cold.
("Harry" "is" "cold" "-")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
triple10
((triple9) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple9) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple10) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple9) -> (rule7 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2