Bob is cold. Bob is smart. Charlie is blue. Charlie is cold. Charlie is nice. Charlie is quiet. Charlie is round. Charlie is smart. Charlie is white. Dave is blue. Dave is cold. Dave is nice. Dave is quiet. Dave is round. Dave is smart. If something is white and nice then it is blue. Smart things are nice.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If something is white and nice then it is blue.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Dave is round.
True
1
proof
[(triple14)]
("Dave" "is" "round" "+")
triple14
Charlie is not round.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "round" "-")
triple7
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is cold.[(triple1)] Bob is smart.[(triple2)] Charlie is blue.[(triple3 OR ((triple9 triple5) -> rule1) OR ((triple9 ((triple8) -> rule2)) -> rule1))] Charlie is cold.[(triple4)] Charlie is nice.[(triple5 OR ((triple8) -> rule2))] Charlie is quiet.[(triple6)] Charlie is round.[(triple7)] Charlie is smart.[(triple8)] Charlie is white.[(triple9)] Dave is blue.[(triple10)] Dave is cold.[(triple11)] Dave is nice.[(triple12 OR ((triple15) -> rule2))] Dave is quiet.[(triple13)] Dave is round.[(triple14)] Dave is smart.[(triple15)] @1: Bob is nice.[(((triple2) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
((triple9 triple5) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple9 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
((triple8) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Dave is blue.
("Dave" "is" "blue" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
((triple15) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple13
Dave is round.
("Dave" "is" "round" "+")
triple14
Dave is smart.
("Dave" "is" "smart" "+")
triple15
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1