Charlie is white. Dave is big. Fiona is not big. Gary is not smart. If someone is furry and not red then they are round. If someone is big then they are round. If someone is furry and not big then they are smart. If someone is blue and furry then they are not smart. If someone is round then they are blue. If someone is big and red then they are blue. If someone is round and not red then they are furry. If Dave is blue then Dave is furry.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Gary is not smart.
("Gary" "is" "smart" "-")
If someone is furry and not red then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "round" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is furry and not big then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "smart" "+"))
If someone is blue and furry then they are not smart.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "-"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is big and red then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is round and not red then they are furry.
((("someone" "is" "round" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "furry" "+"))
If Dave is blue then Dave is furry.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "furry" "+"))
Fiona is not big.
True
1
proof
[(triple3)]
("Fiona" "is" "big" "-")
triple3
Gary is smart.
False
1
inv-proof
[(triple4)]
("Gary" "is" "smart" "+")
triple4
Dave is round.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "round" "+")
((triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "round" "-")
((triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
True
3
proof
[(((((triple2) -> rule2)) -> rule5))]
("Dave" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("Dave" "is" "blue" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
True
4
proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule8))]
("Dave" "is" "furry" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not furry.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule8))]
("Dave" "is" "furry" "-")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "+")
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "furry" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "furry" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Charlie is white.[(triple1)] Dave is big.[(triple2)] Fiona is not big.[(triple3)] Gary is not smart.[(triple4)] @1: Dave is round.[(((triple2) -> rule2))] @2: Dave is blue.[(((((triple2) -> rule2)) -> rule5))] @3: Dave is furry.[(((((((triple2) -> rule2)) -> rule5)) -> rule8))] @4: Dave is not smart.[(((((((triple2) -> rule2)) -> rule5) ((((((triple2) -> rule2)) -> rule5)) -> rule8)) -> rule4))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Fiona is not big.
("Fiona" "is" "big" "-")
triple3
Gary is not smart.
("Gary" "is" "smart" "-")
triple4
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not smart.
("Dave" "is" "smart" "-")
((((((triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4