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