Charlie is kind. Erin is big. Erin is kind. Erin is nice. Fiona is nice. Fiona is quiet. Fiona is rough. If Erin is not kind then Erin is not rough. If someone is cold then they are quiet. Kind, cold people are nice. If Charlie is kind and Charlie is blue then Charlie is cold. If someone is kind and not quiet then they are rough. All nice people are rough.
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If Erin is not kind then Erin is not rough.
((("Erin" "is" "kind" "~")) -> ("Erin" "is" "rough" "-"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Kind, cold people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is kind and Charlie is blue then Charlie is cold.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "cold" "+"))
If someone is kind and not quiet then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "rough" "+"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Fiona is rough.
True
1
proof
[(triple7 OR ((triple5) -> rule6))]
("Fiona" "is" "rough" "+")
triple7
((triple5) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Erin is not nice.
False
1
inv-proof
[(triple4)]
("Erin" "is" "nice" "-")
triple4
Erin is rough.
True
2
proof
[(((triple4) -> rule6))]
("Erin" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple4) -> rule6))]
("Erin" "is" "rough" "-")
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is quiet.
Unknown
rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Charlie is kind.[(triple1)] Erin is big.[(triple2)] Erin is kind.[(triple3)] Erin is nice.[(triple4)] Fiona is nice.[(triple5)] Fiona is quiet.[(triple6)] Fiona is rough.[(triple7 OR ((triple5) -> rule6))] @1: Erin is rough.[(((triple4) -> rule6))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
((triple5) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1