Anne is smart. Dave is blue. Fiona is round. Gary is kind. All furry, kind people are smart. If someone is smart and red then they are blue. If Dave is kind and Dave is smart then Dave is blue. If Dave is furry and Dave is smart then Dave is green. Smart people are furry. Smart, blue people are round. Furry people are red. Furry, round people are green.
Anne is smart.
("Anne" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All furry, kind people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and red then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Dave is kind and Dave is smart then Dave is blue.
((("Dave" "is" "kind" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "blue" "+"))
If Dave is furry and Dave is smart then Dave is green.
((("Dave" "is" "furry" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "green" "+"))
Smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Smart, blue people are round.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Furry, round people are green.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Dave is blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Fiona is not round.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "round" "-")
triple3
Anne is furry.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "furry" "-")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Fiona is not furry.
Unknown
inv-rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Anne is smart.[(triple1)] Dave is blue.[(triple2)] Fiona is round.[(triple3)] Gary is kind.[(triple4)] @1: Anne is furry.[(((triple1) -> rule5))] @2: Anne is red.[(((((triple1) -> rule5)) -> rule7))] @3: Anne is blue.[(((triple1 ((((triple1) -> rule5)) -> rule7)) -> rule2))] @4: Anne is round.[(((triple1 ((triple1 ((((triple1) -> rule5)) -> rule7)) -> rule2)) -> rule6))] @5: Anne is green.[(((((triple1) -> rule5) ((triple1 ((triple1 ((((triple1) -> rule5)) -> rule7)) -> rule2)) -> rule6)) -> rule8))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((triple1 ((triple1 ((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule5 % int5)) ((triple1 ((triple1 ((((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5