Anne is red. Bob is furry. Fiona is round. Harry is kind. All big things are round. All blue, quiet things are furry. All furry things are big. All blue, furry things are big. If something is kind then it is quiet. If Fiona is quiet then Fiona is kind.
Anne is red.
("Anne" "is" "red" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All blue, quiet things are furry.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All blue, furry things are big.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is kind then it is quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If Fiona is quiet then Fiona is kind.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "kind" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Harry is not kind.
False
1
inv-proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Harry is quiet.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "big" "-")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Bob" "is" "round" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Bob" "is" "round" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "furry" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "big" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Anne is red.[(triple1)] Bob is furry.[(triple2)] Fiona is round.[(triple3)] Harry is kind.[(triple4)] @1: Bob is big.[(((triple2) -> rule3))] Harry is quiet.[(((triple4) -> rule5))] @2: Bob is round.[(((((triple2) -> rule3)) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2