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