Anne is young. Dave is round. Erin is smart. Gary is round. If Erin is red and Erin is kind then Erin is round. Young, round people are red. If Dave is smart and Dave is white then Dave is kind. If Dave is young then Dave is kind. If someone is smart then they are blue. If someone is red and young then they are blue. Young people are kind. All blue people are kind.
Anne is young.
("Anne" "is" "young" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is round.
("Gary" "is" "round" "+")
If Erin is red and Erin is kind then Erin is round.
((("Erin" "is" "red" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "round" "+"))
Young, round people are red.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If Dave is smart and Dave is white then Dave is kind.
((("Dave" "is" "smart" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "kind" "+"))
If Dave is young then Dave is kind.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "kind" "+"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and young then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Dave is round.
True
1
proof
[(triple2)]
("Dave" "is" "round" "+")
triple2
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Erin is blue.
True
2
proof
[(((triple3) -> rule5))]
("Erin" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "kind" "-")
((triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "red" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Anne is young.[(triple1)] Dave is round.[(triple2)] Erin is smart.[(triple3)] Gary is round.[(triple4)] @1: Anne is kind.[(((triple1) -> rule7))] Erin is blue.[(((triple3) -> rule5))] @2: Erin is kind.[(((((triple3) -> rule5)) -> rule8))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2