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