Anne is furry. Charlie is cold. Dave is white. Erin is quiet. If someone is furry then they are white. If Charlie is cold then Charlie is furry.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If someone is furry then they are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If Charlie is cold then Charlie is furry.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "furry" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple4)]
("Erin" "is" "quiet" "-")
triple4
Anne is white.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "white" "-")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is white.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "white" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "white" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is furry.[(triple1)] Charlie is cold.[(triple2)] Dave is white.[(triple3)] Erin is quiet.[(triple4)] @1: Anne is white.[(((triple1) -> rule1))] Charlie is furry.[(((triple2) -> rule2))] @2: Charlie is white.[(((((triple2) -> rule2)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2