Anne is smart. Bob is cold. Dave is not blue. Erin is smart. If someone is smart then they are young. Blue people are not young. If someone is young and smart then they are not kind.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Erin is smart.
("Erin" "is" "smart" "+")
If someone is smart then they are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Blue people are not young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "-"))
If someone is young and smart then they are not kind.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "-"))
Erin is smart.
True
1
proof
[(triple4)]
("Erin" "is" "smart" "+")
triple4
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Erin is young.
True
2
proof
[(((triple4) -> rule1))]
("Erin" "is" "young" "+")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple4) -> rule1))]
("Erin" "is" "young" "-")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not kind.
True
4
proof
[(((((triple4) -> rule1) triple4) -> rule3))]
("Erin" "is" "kind" "-")
((((triple4) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is kind.
False
4
inv-proof
[(((((triple4) -> rule1) triple4) -> rule3))]
("Erin" "is" "kind" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is smart.[(triple1)] Bob is cold.[(triple2)] Dave is not blue.[(triple3)] Erin is smart.[(triple4)] @1: Anne is young.[(((triple1) -> rule1))] Erin is young.[(((triple4) -> rule1))] @2: Anne is not kind.[(((((triple1) -> rule1) triple1) -> rule3))] Erin is not kind.[(((((triple4) -> rule1) triple4) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Dave is not blue.
("Dave" "is" "blue" "-")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Erin is not kind.
("Erin" "is" "kind" "-")
((((triple4) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2