Bob is smart. Charlie is nice. Dave is nice. Harry is nice. All round things are not white. If something is white and cold then it is nice. All white, red things are nice. If Charlie is cold then Charlie is red. If Dave is nice then Dave is white. If something is round and not rough then it is cold. If Charlie is white then Charlie is round. Nice, white things are red.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All round things are not white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
If something is white and cold then it is nice.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All white, red things are nice.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If Charlie is cold then Charlie is red.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "red" "+"))
If Dave is nice then Dave is white.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "white" "+"))
If something is round and not rough then it is cold.
((("something" "is" "round" "+") ("something" "is" "rough" "~")) -> ("something" "is" "cold" "+"))
If Charlie is white then Charlie is round.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "round" "+"))
Nice, white things are red.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Harry is nice.
True
1
proof
[(triple4)]
("Harry" "is" "nice" "+")
triple4
Dave is not nice.
False
1
inv-proof
[(triple3)]
("Dave" "is" "nice" "-")
triple3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Bob is smart.[(triple1)] Charlie is nice.[(triple2)] Dave is nice.[(triple3)] Harry is nice.[(triple4)] @1: Dave is white.[(((triple3) -> rule5))] @2: Dave is red.[(((triple3 ((triple3) -> rule5)) -> rule8))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2