Anne is big. Anne is blue. Anne is kind. Anne is red. Anne is smart. Anne is white. Charlie is big. Charlie is not kind. Charlie is not nice. Erin is not big. Erin is blue. Erin is kind. Erin is nice. Erin is not smart. Erin is white. All blue, big people are nice. If someone is red and not kind then they are nice. If Anne is smart then Anne is white. If Charlie is red and Charlie is not blue then Charlie is smart. If someone is nice and kind then they are red. All kind, big people are white. Nice, blue people are white. If someone is blue and not smart then they are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Erin is not big.
("Erin" "is" "big" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is white.
("Erin" "is" "white" "+")
All blue, big people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and not kind then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "nice" "+"))
If Anne is smart then Anne is white.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "white" "+"))
If Charlie is red and Charlie is not blue then Charlie is smart.
((("Charlie" "is" "red" "+") ("Charlie" "is" "blue" "~")) -> ("Charlie" "is" "smart" "+"))
If someone is nice and kind then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All kind, big people are white.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Nice, blue people are white.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is blue and not smart then they are white.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "white" "+"))
Erin is white.
True
1
proof
[(triple15 OR ((triple11 triple14) -> rule8) OR ((triple13 triple11) -> rule7))]
("Erin" "is" "white" "+")
triple15
((triple11 triple14) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple13 triple11) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is not smart.
False
1
inv-proof
[(triple5)]
("Anne" "is" "smart" "-")
triple5
Erin is red.
True
3
proof
[(((triple13 triple12) -> rule5))]
("Erin" "is" "red" "+")
((triple13 triple12) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
3
inv-proof
[(((triple13 triple12) -> rule5))]
("Erin" "is" "red" "-")
((triple13 triple12) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is kind.[(triple3)] Anne is red.[(triple4 OR ((((triple2 triple1) -> rule1) triple3) -> rule5))] Anne is smart.[(triple5)] Anne is white.[(triple6 OR ((triple5) -> rule3) OR ((triple3 triple1) -> rule6) OR ((((triple2 triple1) -> rule1) triple2) -> rule7))] Charlie is big.[(triple7)] Charlie is not kind.[(triple8)] Charlie is not nice.[(triple9)] Erin is blue.[(triple11)] Erin is kind.[(triple12)] Erin is nice.[(triple13)] Erin is not big.[(triple10)] Erin is not smart.[(triple14)] Erin is white.[(triple15 OR ((triple11 triple14) -> rule8) OR ((triple13 triple11) -> rule7))] @1: Anne is nice.[(((triple2 triple1) -> rule1))] Erin is red.[(((triple13 triple12) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((((triple2 triple1) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple5) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple3 triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple2 triple1) -> (rule1 % int2)) triple2) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
triple7
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple8
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple9
Erin is blue.
("Erin" "is" "blue" "+")
triple11
Erin is kind.
("Erin" "is" "kind" "+")
triple12
Erin is nice.
("Erin" "is" "nice" "+")
triple13
Erin is not big.
("Erin" "is" "big" "-")
triple10
Erin is not smart.
("Erin" "is" "smart" "-")
triple14
Erin is white.
("Erin" "is" "white" "+")
triple15
((triple11 triple14) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple13 triple11) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple2 triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple13 triple12) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1