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