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