Anne is rough. Charlie is cold. Dave is cold. Gary is blue. All big, furry things are blue. If something is quiet then it is rough. All blue things are cold. If Charlie is rough and Charlie is blue then Charlie is furry. If something is cold then it is quiet. All furry things are rough.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Gary is blue.
("Gary" "is" "blue" "+")
All big, furry things are blue.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If Charlie is rough and Charlie is blue then Charlie is furry.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "furry" "+"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Dave is cold.
True
1
proof
[(triple3)]
("Dave" "is" "cold" "+")
triple3
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple3) -> rule5))]
("Dave" "is" "quiet" "-")
((triple3) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
True
3
proof
[(((((triple3) -> rule5)) -> rule2))]
("Dave" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("Gary" "is" "quiet" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is rough.
True
4
proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
("Gary" "is" "rough" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not rough.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
("Gary" "is" "rough" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@3: Anne is quiet.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "+")
Charlie is not furry.
Unknown
inv-rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Charlie" "is" "furry" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is rough.[(triple1)] Charlie is cold.[(triple2)] Dave is cold.[(triple3)] Gary is blue.[(triple4)] @1: Charlie is quiet.[(((triple2) -> rule5))] Dave is quiet.[(((triple3) -> rule5))] Gary is cold.[(((triple4) -> rule3))] @2: Charlie is rough.[(((((triple2) -> rule5)) -> rule2))] Dave is rough.[(((((triple3) -> rule5)) -> rule2))] Gary is quiet.[(((((triple4) -> rule3)) -> rule5))] @3: Gary is rough.[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3