Bob is green. Dave is red. Gary is not furry. If someone is green then they are red. If someone is red then they are quiet. If someone is green and not quiet then they are not big. If someone is cold and not big then they are not furry. All quiet, red people are furry. If someone is green and cold then they are furry.
Bob is green.
("Bob" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green and not quiet then they are not big.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "big" "-"))
If someone is cold and not big then they are not furry.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "-"))
All quiet, red people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If someone is green and cold then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Gary is not furry.
True
1
proof
[(triple3)]
("Gary" "is" "furry" "-")
triple3
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Dave is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule5))]
("Dave" "is" "furry" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
True
6
proof
[(((((((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule5))]
("Bob" "is" "furry" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not furry.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule5))]
("Bob" "is" "furry" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is quiet.
Unknown
rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "quiet" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is green.[(triple1)] Dave is red.[(triple2)] Gary is not furry.[(triple3)] @1: Bob is red.[(((triple1) -> rule1))] Dave is quiet.[(((triple2) -> rule2))] @2: Bob is quiet.[(((((triple1) -> rule1)) -> rule2))] Dave is furry.[(((((triple2) -> rule2) triple2) -> rule5))] @3: Bob is furry.[(((((((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule5))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Gary is not furry.
("Gary" "is" "furry" "-")
triple3
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3