Anne is big. Anne is blue. Anne is furry. Anne is kind. Anne is nice. Anne is white. Fiona is furry. Fiona is kind. Fiona is nice. Harry is big. Harry is blue. Harry is furry. Harry is kind. Harry is nice. Harry is round. Harry is white. All kind things are nice. If Anne is furry and Anne is blue then Anne is big. All furry, white things are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If Anne is furry and Anne is blue then Anne is big.
((("Anne" "is" "furry" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "big" "+"))
All furry, white things are round.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Anne is big.
True
1
proof
[(triple1 OR ((triple3 triple2) -> rule2))]
("Anne" "is" "big" "+")
triple1
((triple3 triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is not furry.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "furry" "-")
triple7
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Anne is big.[(triple1 OR ((triple3 triple2) -> rule2))] Anne is blue.[(triple2)] Anne is furry.[(triple3)] Anne is kind.[(triple4)] Anne is nice.[(triple5 OR ((triple4) -> rule1))] Anne is white.[(triple6)] Fiona is furry.[(triple7)] Fiona is kind.[(triple8)] Fiona is nice.[(triple9 OR ((triple8) -> rule1))] Harry is big.[(triple10)] Harry is blue.[(triple11)] Harry is furry.[(triple12)] Harry is kind.[(triple13)] Harry is nice.[(triple14 OR ((triple13) -> rule1))] Harry is round.[(triple15 OR ((triple12 triple16) -> rule3))] Harry is white.[(triple16)] @1: Anne is round.[(((triple3 triple6) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3 triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
((triple4) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
((triple8) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
((triple13) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple15
((triple12 triple16) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple16
Anne is round.
("Anne" "is" "round" "+")
((triple3 triple6) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1