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