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