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