Anne is cold. Bob is cold. Dave is kind. Gary is quiet. Cold people are smart. Young, smart people are kind. Smart people are kind. All quiet people are nice. If someone is cold then they are white. Nice people are smart.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Young, smart people are kind.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold then they are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Gary is nice.
True
2
proof
[(((triple4) -> rule4))]
("Gary" "is" "nice" "+")
((triple4) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple4) -> rule4))]
("Gary" "is" "nice" "-")
((triple4) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
True
3
proof
[(((((triple4) -> rule4)) -> rule6))]
("Gary" "is" "smart" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule6))]
("Gary" "is" "smart" "-")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
True
4
proof
[(((((((triple4) -> rule4)) -> rule6)) -> rule3))]
("Gary" "is" "kind" "+")
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not kind.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule6)) -> rule3))]
("Gary" "is" "kind" "-")
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "white" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "nice" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "white" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is cold.[(triple1)] Bob is cold.[(triple2)] Dave is kind.[(triple3)] Gary is quiet.[(triple4)] @1: Anne is smart.[(((triple1) -> rule1))] Anne is white.[(((triple1) -> rule5))] Bob is smart.[(((triple2) -> rule1))] Bob is white.[(((triple2) -> rule5))] Gary is nice.[(((triple4) -> rule4))] @2: Anne is kind.[(((((triple1) -> rule1)) -> rule3))] Bob is kind.[(((((triple2) -> rule1)) -> rule3))] Gary is smart.[(((((triple4) -> rule4)) -> rule6))] @3: Gary is kind.[(((((((triple4) -> rule4)) -> rule6)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple4) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3