Bob is big. Bob is green. Bob is smart. Dave is blue. Dave is not round. Harry is cold. Harry is not green. If someone is white and big then they are green. All blue people are big. If someone is white and not cold then they are blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not round.
("Dave" "is" "round" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not green.
("Harry" "is" "green" "-")
If someone is white and big then they are green.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone is white and not cold then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "blue" "+"))
Harry is not green.
True
1
proof
[(triple7)]
("Harry" "is" "green" "-")
triple7
Harry is green.
False
1
inv-proof
[(triple7)]
("Harry" "is" "green" "+")
triple7
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "blue" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is smart.[(triple3)] Dave is blue.[(triple4)] Dave is not round.[(triple5)] Harry is cold.[(triple6)] Harry is not green.[(triple7)] @1: Dave is big.[(((triple4) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is not round.
("Dave" "is" "round" "-")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is not green.
("Harry" "is" "green" "-")
triple7
Dave is big.
("Dave" "is" "big" "+")
((triple4) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1