Bob is nice. Bob is white. Charlie is cold. Charlie is kind. Charlie is red. Harry is big. Harry is not kind. Harry is nice. Harry is not red. Harry is not white. If Charlie is red then Charlie is white. Big people are furry. White people are red. Big people are nice. Red people are big. If someone is cold and not big then they are kind.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is not white.
("Harry" "is" "white" "-")
If Charlie is red then Charlie is white.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "white" "+"))
Big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is cold and not big then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "kind" "+"))
Harry is not kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "-")
triple7
Charlie is not kind.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "kind" "-")
triple4
Charlie is big.
True
2
proof
[(((triple5) -> rule5))]
("Charlie" "is" "big" "+")
((triple5) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple5) -> rule1))]
("Charlie" "is" "white" "-")
((triple5) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Bob is big.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("Bob" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule2))]
("Charlie" "is" "furry" "-")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Bob is furry.
True
4
proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule2))]
("Bob" "is" "furry" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not furry.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule2))]
("Bob" "is" "furry" "-")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is nice.[(triple1 OR ((((((triple2) -> rule3)) -> rule5)) -> rule4))] Bob is white.[(triple2)] Charlie is cold.[(triple3)] Charlie is kind.[(triple4)] Charlie is red.[(triple5)] Harry is big.[(triple6)] Harry is nice.[(triple8 OR ((triple6) -> rule4))] Harry is not kind.[(triple7)] Harry is not red.[(triple9)] Harry is not white.[(triple10)] @1: Bob is red.[(((triple2) -> rule3))] Charlie is big.[(((triple5) -> rule5))] Charlie is white.[(((triple5) -> rule1))] Harry is furry.[(((triple6) -> rule2))] @2: Bob is big.[(((((triple2) -> rule3)) -> rule5))] Charlie is furry.[(((((triple5) -> rule5)) -> rule2))] Charlie is nice.[(((((triple5) -> rule5)) -> rule4))] @3: Bob is furry.[(((((((triple2) -> rule3)) -> rule5)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple6) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
triple7
Harry is not red.
("Harry" "is" "red" "-")
triple9
Harry is not white.
("Harry" "is" "white" "-")
triple10
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple5) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple5) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple6) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3