Anne is kind. Anne is nice. Anne is smart. Charlie is cold. Charlie is kind. Charlie is red. Charlie is rough. Fiona is cold. Fiona is kind. Fiona is nice. Fiona is rough. Fiona is smart. If someone is rough and cold then they are smart. If Charlie is nice and Charlie is blue then Charlie is red. All kind people are red. All nice people are smart. All kind people are red. All red, blue people are rough.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is rough and cold then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is nice and Charlie is blue then Charlie is red.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "red" "+"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All red, blue people are rough.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Fiona is smart.
True
1
proof
[(triple12 OR ((triple10) -> rule4) OR ((triple11 triple8) -> rule1))]
("Fiona" "is" "smart" "+")
triple12
((triple10) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple11 triple8) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not kind.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "kind" "-")
triple9
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "rough" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Anne is kind.[(triple1)] Anne is nice.[(triple2)] Anne is smart.[(triple3 OR ((triple2) -> rule4))] Charlie is cold.[(triple4)] Charlie is kind.[(triple5)] Charlie is red.[(triple6 OR ((triple5) -> rule3) OR ((triple5) -> rule5))] Charlie is rough.[(triple7)] Fiona is cold.[(triple8)] Fiona is kind.[(triple9)] Fiona is nice.[(triple10)] Fiona is rough.[(triple11)] Fiona is smart.[(triple12 OR ((triple10) -> rule4) OR ((triple11 triple8) -> rule1))] @1: Anne is red.[(((triple1) -> rule3) OR ((triple1) -> rule5))] Charlie is smart.[(((triple7 triple4) -> rule1))] Fiona is red.[(((triple9) -> rule3) OR ((triple9) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
((triple5) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple5) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
((triple10) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple11 triple8) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple7 triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple9) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple9) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1