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