Bob is blue. Bob is nice. Bob is smart. Harry is green. Harry is nice. Harry is quiet. Harry is smart. Quiet, nice things are blue. White things are nice. If Bob is white and Bob is smart then Bob is nice. If Harry is quiet and Harry is nice then Harry is white. If something is white then it is nice. Quiet, blue things are green. If something is cold and green then it is smart. If Harry is green then Harry is blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Quiet, nice things are blue.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
White things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If Bob is white and Bob is smart then Bob is nice.
((("Bob" "is" "white" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "nice" "+"))
If Harry is quiet and Harry is nice then Harry is white.
((("Harry" "is" "quiet" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "white" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Quiet, blue things are green.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is cold and green then it is smart.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Harry is green then Harry is blue.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "blue" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Bob is smart.[(triple3)] Harry is green.[(triple4 OR ((triple6 ((triple6 triple5) -> rule1)) -> rule6))] Harry is nice.[(triple5)] Harry is quiet.[(triple6)] Harry is smart.[(triple7)] @1: Harry is blue.[(((triple4) -> rule8) OR ((triple6 triple5) -> rule1))] Harry is white.[(((triple6 triple5) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
((triple6 ((triple6 triple5) -> (rule1 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple6 triple5) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple6 triple5) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1