Anne is big. Anne is kind. Anne is red. Gary is big. Gary is red. Gary is rough. Harry is red. All quiet things are kind. All big, furry things are red. If something is big then it is rough. If something is rough then it is red. If something is rough then it is furry. If something is quiet then it is kind. If something is kind and furry then it is quiet. If something is furry then it is red.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is red.
("Harry" "is" "red" "+")
All quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All big, furry things are red.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is rough then it is furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is kind and furry then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Gary is rough.
True
1
proof
[(triple6 OR ((triple4) -> rule3))]
("Gary" "is" "rough" "+")
triple6
((triple4) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is not red.
False
1
inv-proof
[(triple7)]
("Harry" "is" "red" "-")
triple7
Harry is not kind.
Unknown
inv-rconc
[@3: Harry is kind.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule6 <- FAIL)]]
("Harry" "is" "kind" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Anne is red.[(triple3 OR ((((triple1) -> rule3)) -> rule4) OR ((((((triple1) -> rule3)) -> rule5)) -> rule8) OR ((triple1 ((((triple1) -> rule3)) -> rule5)) -> rule2))] Gary is big.[(triple4)] Gary is red.[(triple5 OR ((triple6) -> rule4) OR ((((triple4) -> rule3)) -> rule4) OR ((((triple6) -> rule5)) -> rule8) OR ((triple4 ((triple6) -> rule5)) -> rule2) OR ((((((triple4) -> rule3)) -> rule5)) -> rule8) OR ((triple4 ((((triple4) -> rule3)) -> rule5)) -> rule2))] Gary is rough.[(triple6 OR ((triple4) -> rule3))] Harry is red.[(triple7)] @1: Anne is rough.[(((triple1) -> rule3))] Gary is furry.[(((triple6) -> rule5) OR ((((triple4) -> rule3)) -> rule5))] @2: Anne is furry.[(((((triple1) -> rule3)) -> rule5))] @3: Anne is quiet.[(((triple2 ((((triple1) -> rule3)) -> rule5)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
((triple6) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((triple4 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
triple6
((triple4) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple6) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3