Anne is nice. Charlie is blue. Dave is smart. Erin is nice. All white, young people are big. If someone is young and big then they are white. If someone is smart then they are round.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
All white, young people are big.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is young and big then they are white.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Erin is nice.
True
1
proof
[(triple4)]
("Erin" "is" "nice" "+")
triple4
Erin is not nice.
False
1
inv-proof
[(triple4)]
("Erin" "is" "nice" "-")
triple4
Dave is round.
True
2
proof
[(((triple3) -> rule3))]
("Dave" "is" "round" "+")
((triple3) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple3) -> rule3))]
("Dave" "is" "round" "-")
((triple3) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "big" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is nice.[(triple1)] Charlie is blue.[(triple2)] Dave is smart.[(triple3)] Erin is nice.[(triple4)] @1: Dave is round.[(((triple3) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1