Anne is furry. Dave is big. Fiona is round. Harry is round. White, blue people are furry. If someone is round then they are white. If someone is furry then they are blue. All round people are white. Round people are big. All big people are round.
Anne is furry.
("Anne" "is" "furry" "+")
Dave is big.
("Dave" "is" "big" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is round.
("Harry" "is" "round" "+")
White, blue people are furry.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is furry then they are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Fiona is not round.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "round" "-")
triple3
Fiona is white.
True
2
proof
[(((triple3) -> rule2) OR ((triple3) -> rule4))]
("Fiona" "is" "white" "+")
((triple3) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple3) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "big" "-")
((triple4) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Dave is white.
True
3
proof
[(((((triple2) -> rule6)) -> rule2) OR ((((triple2) -> rule6)) -> rule4))]
("Dave" "is" "white" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2) OR ((((triple2) -> rule6)) -> rule4))]
("Dave" "is" "white" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Anne is not round.
Unknown
inv-rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is white.
Unknown
rconc
[@3: Anne is white.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule5 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Anne" "is" "big" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
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 furry.[(triple1)] Dave is big.[(triple2)] Fiona is round.[(triple3)] Harry is round.[(triple4)] @1: Anne is blue.[(((triple1) -> rule3))] Dave is round.[(((triple2) -> rule6))] Fiona is big.[(((triple3) -> rule5))] Fiona is white.[(((triple3) -> rule2) OR ((triple3) -> rule4))] Harry is big.[(((triple4) -> rule5))] Harry is white.[(((triple4) -> rule2) OR ((triple4) -> rule4))] @2: Dave is white.[(((((triple2) -> rule6)) -> rule2) OR ((((triple2) -> rule6)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple3) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple3) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple4) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2