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