Anne is blue. Anne is furry. Bob is rough. Bob is white. Charlie is cold. Charlie is round. Charlie is white. Harry is blue. Harry is cold. Harry is furry. Harry is rough. Harry is round. Cold, furry things are round. All smart things are furry. Smart things are blue. All cold, rough things are blue. All round, cold things are blue. Round, rough things are blue. Cold, round things are white. If Harry is rough and Harry is round then Harry is furry.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Cold, furry things are round.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All cold, rough things are blue.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All round, cold things are blue.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Round, rough things are blue.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Cold, round things are white.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Harry is rough and Harry is round then Harry is furry.
((("Harry" "is" "rough" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "furry" "+"))
Anne is furry.
True
1
proof
[(triple2)]
("Anne" "is" "furry" "+")
triple2
Charlie is not round.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "round" "-")
triple6
Charlie is blue.
True
3
proof
[(((triple6 triple5) -> rule5))]
("Charlie" "is" "blue" "+")
((triple6 triple5) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Harry is not white.
False
3
inv-proof
[(((triple9 triple12) -> rule7) OR ((triple9 ((triple9 triple10) -> rule1)) -> rule7))]
("Harry" "is" "white" "-")
((triple9 triple12) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple9 ((triple9 triple10) -> (rule1 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "white" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Bob is rough.[(triple3)] Bob is white.[(triple4)] Charlie is cold.[(triple5)] Charlie is round.[(triple6)] Charlie is white.[(triple7 OR ((triple5 triple6) -> rule7))] Harry is blue.[(triple8 OR ((triple12 triple11) -> rule6) OR ((triple12 triple9) -> rule5) OR ((triple9 triple11) -> rule4) OR ((((triple9 triple10) -> rule1) triple11) -> rule6) OR ((((triple9 triple10) -> rule1) triple9) -> rule5))] Harry is cold.[(triple9)] Harry is furry.[(triple10 OR ((triple11 triple12) -> rule8))] Harry is rough.[(triple11)] Harry is round.[(triple12 OR ((triple9 triple10) -> rule1))] @1: Charlie is blue.[(((triple6 triple5) -> rule5))] Harry is white.[(((triple9 triple12) -> rule7) OR ((triple9 ((triple9 triple10) -> rule1)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple5 triple6) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple8
((triple12 triple11) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple12 triple9) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple9 triple11) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple9 triple10) -> (rule1 % int2)) triple11) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple9 triple10) -> (rule1 % int2)) triple9) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
((triple11 triple12) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
((triple9 triple10) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple6 triple5) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple9 triple12) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple9 ((triple9 triple10) -> (rule1 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2