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