Anne is blue. Bob is young. All smart things are quiet. If something is young and smart then it is quiet. All blue things are smart. All green things are white. If Bob is green then Bob is white. If Anne is quiet then Anne is not red. If Anne is blue and Anne is white then Anne is young. Green things are red.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is young.
("Bob" "is" "young" "+")
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is young and smart then it is quiet.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If Bob is green then Bob is white.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "white" "+"))
If Anne is quiet then Anne is not red.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "red" "-"))
If Anne is blue and Anne is white then Anne is young.
((("Anne" "is" "blue" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "young" "+"))
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Bob is not young.
False
1
inv-proof
[(triple2)]
("Bob" "is" "young" "-")
triple2
Anne is smart.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is quiet.
Unknown
rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is blue.[(triple1)] Bob is young.[(triple2)] @1: Anne is smart.[(((triple1) -> rule3))] @2: Anne is quiet.[(((((triple1) -> rule3)) -> rule1))] @3: Anne is not red.[(((((((triple1) -> rule3)) -> rule1)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not red.
("Anne" "is" "red" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3