Anne is blue. Anne is red. Anne is white. Bob is rough. Bob is round. Bob is white. Dave is round. All kind, red people are smart. If Bob is blue and Bob is red then Bob is kind. Kind, blue people are smart. If someone is smart and blue then they are round. If Dave is blue and Dave is rough then Dave is red. All red people are round. If Dave is rough then Dave is red. Red people are smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is round.
("Dave" "is" "round" "+")
All kind, red people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If Bob is blue and Bob is red then Bob is kind.
((("Bob" "is" "blue" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "kind" "+"))
Kind, blue people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and blue then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Dave is blue and Dave is rough then Dave is red.
((("Dave" "is" "blue" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "red" "+"))
All red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If Dave is rough then Dave is red.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "red" "+"))
Red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Anne is red.
True
1
proof
[(triple2)]
("Anne" "is" "red" "+")
triple2
Bob is not rough.
False
1
inv-proof
[(triple4)]
("Bob" "is" "rough" "-")
triple4
Anne is smart.
True
2
proof
[(((triple2) -> rule8))]
("Anne" "is" "smart" "+")
((triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple2) -> rule8))]
("Anne" "is" "smart" "-")
((triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "red" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is red.[(triple2)] Anne is white.[(triple3)] Bob is rough.[(triple4)] Bob is round.[(triple5)] Bob is white.[(triple6)] Dave is round.[(triple7)] @1: Anne is round.[(((triple2) -> rule6) OR ((((triple2) -> rule8) triple1) -> rule4))] Anne is smart.[(((triple2) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1