Anne is white. Bob is white. Charlie is blue. Harry is big. Big things are white. If Harry is round and Harry is red then Harry is white. White, round things are big.
Anne is white.
("Anne" "is" "white" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Harry is round and Harry is red then Harry is white.
((("Harry" "is" "round" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "white" "+"))
White, round things are big.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Bob is white.
True
1
proof
[(triple2)]
("Bob" "is" "white" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "blue" "-")
triple3
Harry is white.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "white" "+")
((triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "white" "-")
((triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Anne is white.[(triple1)] Bob is white.[(triple2)] Charlie is blue.[(triple3)] Harry is big.[(triple4)] @1: Harry is white.[(((triple4) -> rule1))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1