Anne is round. Dave is white. If something is blue and smart then it is red. Smart things are young. All young things are red. If something is smart and blue then it is red. Round things are blue. All furry things are young. If something is red then it is smart. White things are smart.
Anne is round.
("Anne" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
If something is blue and smart then it is red.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is smart and blue then it is red.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is red then it is smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
White things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Anne is not smart.
Unknown
inv-rconc
[@4: Anne is smart.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule2 <- rule8 <- FAIL)]]
("Anne" "is" "smart" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Anne is round.[(triple1)] Dave is white.[(triple2)] @1: Anne is blue.[(((triple1) -> rule5))] Dave is smart.[(((triple2) -> rule8))] @2: Dave is young.[(((((triple2) -> rule8)) -> rule2))] @3: Dave is red.[(((((((triple2) -> rule8)) -> rule2)) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple2) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((((triple2) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3