Bob is cold. Bob is quiet. Bob is red. Gary is quiet. Gary is red. Gary is rough. Gary is white. Harry is quiet. Harry is red. Harry is not rough. If something is nice then it is smart. All cold things are nice.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "-")
triple2
Bob is nice.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Bob" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "nice" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is quiet.[(triple2)] Bob is red.[(triple3)] Gary is quiet.[(triple4)] Gary is red.[(triple5)] Gary is rough.[(triple6)] Gary is white.[(triple7)] Harry is not rough.[(triple10)] Harry is quiet.[(triple8)] Harry is red.[(triple9)] @1: Bob is nice.[(((triple1) -> rule2))] @2: Bob is smart.[(((((triple1) -> rule2)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Harry is not rough.
("Harry" "is" "rough" "-")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2