Bob is not quiet. Charlie is red. Dave is big. Harry is white. All quiet, big people are cold. If someone is big then they are cold. If Dave is red and Dave is nice then Dave is not cold. Cold, kind people are red. All cold people are kind. If someone is quiet and not red then they are white.
Bob is not quiet.
("Bob" "is" "quiet" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Harry is white.
("Harry" "is" "white" "+")
All quiet, big people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If Dave is red and Dave is nice then Dave is not cold.
((("Dave" "is" "red" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "cold" "-"))
Cold, kind people are red.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet and not red then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "white" "+"))
Harry is white.
True
1
proof
[(triple4)]
("Harry" "is" "white" "+")
triple4
Bob is quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Dave is cold.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "cold" "-")
((triple3) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
True
3
proof
[(((((triple3) -> rule2)) -> rule5))]
("Dave" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule5))]
("Dave" "is" "kind" "-")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "+")
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Bob" "is" "red" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Bob is not quiet.[(triple1)] Charlie is red.[(triple2)] Dave is big.[(triple3)] Harry is white.[(triple4)] @1: Dave is cold.[(((triple3) -> rule2))] @2: Dave is kind.[(((((triple3) -> rule2)) -> rule5))] @3: Dave is red.[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule4))]
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3