Charlie is furry. Charlie is green. Charlie is rough. Dave is big. Dave is blue. Dave is green. Dave is rough. All blue things are furry. If something is nice then it is round. If something is blue then it is nice. Nice things are round. If something is green then it is furry. All rough things are furry. All round, furry things are nice. All blue things are big.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
All blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All round, furry things are nice.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Charlie is not furry.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule5) OR ((triple3) -> rule6))]
("Charlie" "is" "furry" "-")
triple1
((triple2) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple3) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is furry.
True
2
proof
[(((triple5) -> rule1) OR ((triple6) -> rule5) OR ((triple7) -> rule6))]
("Dave" "is" "furry" "+")
((triple5) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple6) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple7) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple5) -> rule3))]
("Dave" "is" "nice" "-")
((triple5) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
True
3
proof
[(((((triple5) -> rule3)) -> rule2) OR ((((triple5) -> rule3)) -> rule4))]
("Dave" "is" "round" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule2) OR ((((triple5) -> rule3)) -> rule4))]
("Dave" "is" "round" "-")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Charlie is not round.
Unknown
inv-rconc
[@4: Charlie is round.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule4 <- rule3 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not nice.
Unknown
inv-rconc
[@3: Charlie is nice.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is furry.[(triple1 OR ((triple2) -> rule5) OR ((triple3) -> rule6))] Charlie is green.[(triple2)] Charlie is rough.[(triple3)] Dave is big.[(triple4 OR ((triple5) -> rule8))] Dave is blue.[(triple5)] Dave is green.[(triple6)] Dave is rough.[(triple7)] @1: Dave is furry.[(((triple5) -> rule1) OR ((triple6) -> rule5) OR ((triple7) -> rule6))] Dave is nice.[(((triple5) -> rule3))] @2: Dave is round.[(((((triple5) -> rule3)) -> rule2) OR ((((triple5) -> rule3)) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
((triple2) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple3) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
((triple5) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
((triple5) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple6) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple7) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple5) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2