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