Charlie is kind. Dave is kind. Erin is quiet. Furry, green people are rough. All white, kind people are rough. If someone is kind then they are green. All quiet, kind people are cold. If someone is quiet and green then they are rough. If someone is kind then they are furry. If someone is quiet then they are rough. Furry, rough people are green.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Furry, green people are rough.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All white, kind people are rough.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All quiet, kind people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet and green then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Furry, rough people are green.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple3)]
("Erin" "is" "quiet" "-")
triple3
Charlie is furry.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "green" "-")
((triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
True
5
proof
[(((((triple2) -> rule6) ((triple2) -> rule3)) -> rule1))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule6 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Charlie is not rough.
False
5
inv-proof
[(((((triple1) -> rule6) ((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "furry" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "+")
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Charlie is kind.[(triple1)] Dave is kind.[(triple2)] Erin is quiet.[(triple3)] @1: Charlie is furry.[(((triple1) -> rule6))] Charlie is green.[(((triple1) -> rule3))] Dave is furry.[(((triple2) -> rule6))] Dave is green.[(((triple2) -> rule3))] Erin is rough.[(((triple3) -> rule7))] @2: Charlie is rough.[(((((triple1) -> rule6) ((triple1) -> rule3)) -> rule1))] Dave is rough.[(((((triple2) -> rule6) ((triple2) -> rule3)) -> rule1))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule6 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3