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