Anne is blue. Anne is furry. Anne is smart. Anne is young. Fiona is blue. Fiona is nice. Gary is blue. Gary is young. Harry is blue. Harry is furry. Nice, furry things are kind. All kind things are nice. If something is nice then it is young. All red, furry things are young. If something is young then it is red. Furry, kind things are smart. All red things are furry.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Nice, furry things are kind.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All red, furry things are young.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Furry, kind things are smart.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Fiona is blue.
True
1
proof
[(triple5)]
("Fiona" "is" "blue" "+")
triple5
Anne is not young.
False
1
inv-proof
[(triple4)]
("Anne" "is" "young" "-")
triple4
Anne is red.
True
2
proof
[(((triple4) -> rule5))]
("Anne" "is" "red" "+")
((triple4) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple4) -> rule5))]
("Anne" "is" "red" "-")
((triple4) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Fiona is red.
True
3
proof
[(((((triple6) -> rule3)) -> rule5))]
("Fiona" "is" "red" "+")
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple8) -> rule5)) -> rule7))]
("Gary" "is" "furry" "-")
((((triple8) -> (rule5 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Fiona is furry.
True
4
proof
[(((((((triple6) -> rule3)) -> rule5)) -> rule7))]
("Fiona" "is" "furry" "+")
((((((triple6) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not furry.
False
4
inv-proof
[(((((((triple6) -> rule3)) -> rule5)) -> rule7))]
("Fiona" "is" "furry" "-")
((((((triple6) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is kind.
True
6
proof
[(((triple6 ((((((triple6) -> rule3)) -> rule5)) -> rule7)) -> rule1))]
("Fiona" "is" "kind" "+")
((triple6 ((((((triple6) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is not kind.
False
6
inv-proof
[(((triple6 ((((((triple6) -> rule3)) -> rule5)) -> rule7)) -> rule1))]
("Fiona" "is" "kind" "-")
((triple6 ((((((triple6) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is smart.
True
11
proof
[(((((((((triple6) -> rule3)) -> rule5)) -> rule7) ((triple6 ((((((triple6) -> rule3)) -> rule5)) -> rule7)) -> rule1)) -> rule6))]
("Fiona" "is" "smart" "+")
((((((((triple6) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule7 % int3)) ((triple6 ((((((triple6) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
Fiona is not smart.
False
11
inv-proof
[(((((((((triple6) -> rule3)) -> rule5)) -> rule7) ((triple6 ((((((triple6) -> rule3)) -> rule5)) -> rule7)) -> rule1)) -> rule6))]
("Fiona" "is" "smart" "-")
((((((((triple6) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule7 % int3)) ((triple6 ((((((triple6) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
Harry is not young.
Unknown
inv-rconc
[@5: Harry is young.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule3 <- rule2 <- rule1 <- FAIL)]]
("Harry" "is" "young" "-")
Gary is smart.
Unknown
rconc
[@3: Gary is smart.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule2 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "kind" "-")
Harry is kind.
Unknown
rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not nice.
Unknown
inv-rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is red.
Unknown
rconc
[@4: Harry is red.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule2 <- rule1 <- FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2 OR ((((triple4) -> rule5)) -> rule7))] Anne is smart.[(triple3)] Anne is young.[(triple4)] Fiona is blue.[(triple5)] Fiona is nice.[(triple6)] Gary is blue.[(triple7)] Gary is young.[(triple8)] Harry is blue.[(triple9)] Harry is furry.[(triple10)] @1: Anne is red.[(((triple4) -> rule5))] Fiona is young.[(((triple6) -> rule3))] Gary is red.[(((triple8) -> rule5))] @2: Fiona is red.[(((((triple6) -> rule3)) -> rule5))] Gary is furry.[(((((triple8) -> rule5)) -> rule7))] @3: Fiona is furry.[(((((((triple6) -> rule3)) -> rule5)) -> rule7))] @4: Fiona is kind.[(((triple6 ((((((triple6) -> rule3)) -> rule5)) -> rule7)) -> rule1))] @5: Fiona is smart.[(((((((((triple6) -> rule3)) -> rule5)) -> rule7) ((triple6 ((((((triple6) -> rule3)) -> rule5)) -> rule7)) -> rule1)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is young.
("Gary" "is" "young" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Anne is red.
("Anne" "is" "red" "+")
((triple4) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple6) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple8) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple8) -> (rule5 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((((((triple6) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple6 ((((((triple6) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((((triple6) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule7 % int3)) ((triple6 ((((((triple6) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5