Bob is blue. Bob is nice. Bob is round. Gary is big. Gary is nice. Harry is big. Harry is young. If someone is cold and nice then they are kind. All young people are cold. Young, big people are nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is cold and nice then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Young, big people are nice.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Gary is nice.
True
1
proof
[(triple5)]
("Gary" "is" "nice" "+")
triple5
Bob is not round.
False
1
inv-proof
[(triple3)]
("Bob" "is" "round" "-")
triple3
Harry is cold.
True
2
proof
[(((triple7) -> rule2))]
("Harry" "is" "cold" "+")
((triple7) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple7) -> rule2))]
("Harry" "is" "cold" "-")
((triple7) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
True
6
proof
[(((((triple7) -> rule2) ((triple7 triple6) -> rule3)) -> rule1))]
("Harry" "is" "kind" "+")
((((triple7) -> (rule2 % int3)) ((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not kind.
False
6
inv-proof
[(((((triple7) -> rule2) ((triple7 triple6) -> rule3)) -> rule1))]
("Harry" "is" "kind" "-")
((((triple7) -> (rule2 % int3)) ((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is kind.
Unknown
rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "kind" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- 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 blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Bob is round.[(triple3)] Gary is big.[(triple4)] Gary is nice.[(triple5)] Harry is big.[(triple6)] Harry is young.[(triple7)] @1: Harry is cold.[(((triple7) -> rule2))] Harry is nice.[(((triple7 triple6) -> rule3))] @2: Harry is kind.[(((((triple7) -> rule2) ((triple7 triple6) -> rule3)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
((triple7) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7 triple6) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple7) -> (rule2 % int3)) ((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3