Anne is smart. Anne is white. Bob is cold. Bob is nice. Dave is kind. Dave is nice. Dave is red. Dave is young. Erin is cold. Erin is nice. Erin is smart. Erin is young. If something is kind and white then it is smart. All cold things are young. Nice, cold things are kind.
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is kind and white then it is smart.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Nice, cold things are kind.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Erin is young.
True
1
proof
[(triple12 OR ((triple9) -> rule2))]
("Erin" "is" "young" "+")
triple12
((triple9) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Dave is not nice.
False
1
inv-proof
[(triple6)]
("Dave" "is" "nice" "-")
triple6
Erin is kind.
True
3
proof
[(((triple10 triple9) -> rule3))]
("Erin" "is" "kind" "+")
((triple10 triple9) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
3
inv-proof
[(((triple10 triple9) -> rule3))]
("Erin" "is" "kind" "-")
((triple10 triple9) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Anne is smart.[(triple1)] Anne is white.[(triple2)] Bob is cold.[(triple3)] Bob is nice.[(triple4)] Dave is kind.[(triple5)] Dave is nice.[(triple6)] Dave is red.[(triple7)] Dave is young.[(triple8)] Erin is cold.[(triple9)] Erin is nice.[(triple10)] Erin is smart.[(triple11)] Erin is young.[(triple12 OR ((triple9) -> rule2))] @1: Bob is kind.[(((triple4 triple3) -> rule3))] Bob is young.[(((triple3) -> rule2))] Erin is kind.[(((triple10 triple9) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple9) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple4 triple3) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple3) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple10 triple9) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1