Anne is young. Gary is big. Harry is nice. If something is furry then it is nice. Blue, furry things are young. All big things are young. If something is young then it is furry. Young things are not blue. Big things are not blue. Nice, red things are big. If something is nice and not big then it is smart.
Anne is young.
("Anne" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Blue, furry things are young.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is young then it is furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Young things are not blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "-"))
Big things are not blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
Nice, red things are big.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is nice and not big then it is smart.
((("something" "is" "nice" "+") ("something" "is" "big" "~")) -> ("something" "is" "smart" "+"))
Harry is nice.
True
1
proof
[(triple3)]
("Harry" "is" "nice" "+")
triple3
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Gary is not blue.
True
2
proof
[(((triple2) -> rule6) OR ((((triple2) -> rule3)) -> rule5))]
("Gary" "is" "blue" "-")
((triple2) -> (rule6 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "furry" "-")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Gary is furry.
True
3
proof
[(((((triple2) -> rule3)) -> rule4))]
("Gary" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4))]
("Gary" "is" "furry" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
True
4
proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule1))]
("Gary" "is" "nice" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not nice.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule1))]
("Gary" "is" "nice" "-")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "smart" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "smart" "-")
Harry is furry.
Unknown
rconc
[@3: Harry is furry.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule7 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Anne is young.[(triple1)] Gary is big.[(triple2)] Harry is nice.[(triple3)] @1: Anne is furry.[(((triple1) -> rule4))] Anne is not blue.[(((triple1) -> rule5))] Gary is not blue.[(((triple2) -> rule6) OR ((((triple2) -> rule3)) -> rule5))] Gary is young.[(((triple2) -> rule3))] @2: Anne is nice.[(((((triple1) -> rule4)) -> rule1))] Gary is furry.[(((((triple2) -> rule3)) -> rule4))] @3: Gary is nice.[(((((((triple2) -> rule3)) -> rule4)) -> rule1))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
((triple1) -> (rule5 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Gary is not blue.
("Gary" "is" "blue" "-")
((triple2) -> (rule6 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple2) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3