Anne is kind. Bob is kind. Charlie is kind. Dave is not young. If someone is red then they are white. All kind, smart people are not furry. If someone is white and not red then they are smart. All cold people are not young. If someone is smart and not white then they are cold. All kind people are cold. All white people are cold. All young, kind people are cold.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is not young.
("Dave" "is" "young" "-")
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
All kind, smart people are not furry.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "-"))
If someone is white and not red then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "smart" "+"))
All cold people are not young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "-"))
If someone is smart and not white then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "cold" "+"))
All kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All young, kind people are cold.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Dave is not young.
True
1
proof
[(triple4)]
("Dave" "is" "young" "-")
triple4
Dave is young.
False
1
inv-proof
[(triple4)]
("Dave" "is" "young" "+")
triple4
Charlie is cold.
True
2
proof
[(((triple3) -> rule6))]
("Charlie" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "cold" "-")
((triple2) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not young.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("Bob" "is" "young" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Charlie is young.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule4))]
("Charlie" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "smart" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "+")
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is kind.[(triple1)] Bob is kind.[(triple2)] Charlie is kind.[(triple3)] Dave is not young.[(triple4)] @1: Anne is cold.[(((triple1) -> rule6))] Bob is cold.[(((triple2) -> rule6))] Charlie is cold.[(((triple3) -> rule6))] @2: Anne is not young.[(((((triple1) -> rule6)) -> rule4))] Bob is not young.[(((((triple2) -> rule6)) -> rule4))] Charlie is not young.[(((((triple3) -> rule6)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Dave is not young.
("Dave" "is" "young" "-")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is not young.
("Bob" "is" "young" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Charlie is not young.
("Charlie" "is" "young" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2