Bob is nice. Bob is red. Bob is young. Gary is kind. Gary is red. Gary is rough. Gary is young. Cold, nice things are green. All red things are kind. All kind, cold things are nice. All cold, red things are young. Nice things are cold. If Bob is nice and Bob is red then Bob is cold.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
Cold, nice things are green.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All kind, cold things are nice.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All cold, red things are young.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If Bob is nice and Bob is red then Bob is cold.
((("Bob" "is" "nice" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "cold" "+"))
Gary is kind.
True
1
proof
[(triple4 OR ((triple5) -> rule2))]
("Gary" "is" "kind" "+")
triple4
((triple5) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not rough.
False
1
inv-proof
[(triple6)]
("Gary" "is" "rough" "-")
triple6
Bob is cold.
True
2
proof
[(((triple1) -> rule5) OR ((triple1 triple2) -> rule6))]
("Bob" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple1 triple2) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "kind" "-")
((triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
True
4
proof
[(((((triple1) -> rule5) triple1) -> rule1) OR ((((triple1 triple2) -> rule6) triple1) -> rule1))]
("Bob" "is" "green" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple1 triple2) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not green.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule1) OR ((((triple1 triple2) -> rule6) triple1) -> rule1))]
("Bob" "is" "green" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple1 triple2) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Gary is not cold.
Unknown
inv-rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not green.
Unknown
inv-rconc
[@3: Gary is green.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule3 <- FAIL)]]
("Gary" "is" "green" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is nice.[(triple1)] Bob is red.[(triple2)] Bob is young.[(triple3 OR ((((triple1) -> rule5) triple2) -> rule4) OR ((((triple1 triple2) -> rule6) triple2) -> rule4))] Gary is kind.[(triple4 OR ((triple5) -> rule2))] Gary is red.[(triple5)] Gary is rough.[(triple6)] Gary is young.[(triple7)] @1: Bob is cold.[(((triple1) -> rule5) OR ((triple1 triple2) -> rule6))] Bob is kind.[(((triple2) -> rule2))] @2: Bob is green.[(((((triple1) -> rule5) triple1) -> rule1) OR ((((triple1 triple2) -> rule6) triple1) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
((((triple1) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple1 triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple4
((triple5) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple1 triple2) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple1 triple2) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2