Charlie is rough. Erin is nice. Fiona is white. Harry is kind. All white, kind things are quiet. White, big things are kind. Rough things are quiet. If Charlie is rough then Charlie is quiet. If something is big then it is cold. All quiet things are white.
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All white, kind things are quiet.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
White, big things are kind.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is rough then Charlie is quiet.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "quiet" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Harry is kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "+")
triple4
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "cold" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Charlie is rough.[(triple1)] Erin is nice.[(triple2)] Fiona is white.[(triple3)] Harry is kind.[(triple4)] @1: Charlie is quiet.[(((triple1) -> rule3) OR ((triple1) -> rule4))] @2: Charlie is white.[(((((triple1) -> rule3)) -> rule6) OR ((((triple1) -> rule4)) -> rule6))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2