Charlie is quiet. Charlie is round. Charlie is white. Dave is white. Fiona is round. Fiona is white. Harry is white. Rough people are kind. If someone is cold and quiet then they are round. Round, quiet people are rough. If someone is rough and furry then they are cold. All kind, rough people are quiet. If Charlie is rough then Charlie is kind. If someone is cold then they are white. Round, cold people are rough.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold and quiet then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Round, quiet people are rough.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and furry then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All kind, rough people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is rough then Charlie is kind.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "kind" "+"))
If someone is cold then they are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Round, cold people are rough.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Charlie is white.
True
1
proof
[(triple3)]
("Charlie" "is" "white" "+")
triple3
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Charlie is rough.
True
3
proof
[(((triple2 triple1) -> rule3))]
("Charlie" "is" "rough" "+")
((triple2 triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
3
inv-proof
[(((triple2 triple1) -> rule3))]
("Charlie" "is" "rough" "-")
((triple2 triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
True
4
proof
[(((((triple2 triple1) -> rule3)) -> rule1) OR ((((triple2 triple1) -> rule3)) -> rule6))]
("Charlie" "is" "kind" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple2 triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not kind.
False
4
inv-proof
[(((((triple2 triple1) -> rule3)) -> rule1) OR ((((triple2 triple1) -> rule3)) -> rule6))]
("Charlie" "is" "kind" "-")
((((triple2 triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple2 triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is rough.
Unknown
rconc
[@4: Fiona is rough.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule8 <- rule4 <- FAIL)]]
("Fiona" "is" "rough" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule4 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is quiet.[(triple1)] Charlie is round.[(triple2)] Charlie is white.[(triple3)] Dave is white.[(triple4)] Fiona is round.[(triple5)] Fiona is white.[(triple6)] Harry is white.[(triple7)] @1: Charlie is rough.[(((triple2 triple1) -> rule3))] @2: Charlie is kind.[(((((triple2 triple1) -> rule3)) -> rule1) OR ((((triple2 triple1) -> rule3)) -> rule6))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Fiona is round.
("Fiona" "is" "round" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2 triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple2 triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2