Erin is not nice. Fiona is white. Gary is cold. Harry is big. All white things are furry. Furry, round things are blue. If something is blue and not nice then it is cold. If Erin is nice and Erin is white then Erin is not big. All furry things are round. If Gary is white then Gary is not furry. If something is furry and not cold then it is not big. If something is round then it is big.
Erin is not nice.
("Erin" "is" "nice" "-")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is big.
("Harry" "is" "big" "+")
All white things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Furry, round things are blue.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is blue and not nice then it is cold.
((("something" "is" "blue" "+") ("something" "is" "nice" "~")) -> ("something" "is" "cold" "+"))
If Erin is nice and Erin is white then Erin is not big.
((("Erin" "is" "nice" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "big" "-"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Gary is white then Gary is not furry.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "furry" "-"))
If something is furry and not cold then it is not big.
((("something" "is" "furry" "+") ("something" "is" "cold" "~")) -> ("something" "is" "big" "-"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Erin is not nice.
True
1
proof
[(triple1)]
("Erin" "is" "nice" "-")
triple1
Erin is nice.
False
1
inv-proof
[(triple1)]
("Erin" "is" "nice" "+")
triple1
Fiona is furry.
True
2
proof
[(((triple2) -> rule1))]
("Fiona" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is not furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Fiona" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("Fiona" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is not round.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Fiona" "is" "round" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is big.
True
4
proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule8))]
("Fiona" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is not blue.
False
6
inv-proof
[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule5)) -> rule2))]
("Fiona" "is" "blue" "-")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is round.
Unknown
rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "round" "+")
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "furry" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Erin is not nice.[(triple1)] Fiona is white.[(triple2)] Gary is cold.[(triple3)] Harry is big.[(triple4)] @1: Fiona is furry.[(((triple2) -> rule1))] @2: Fiona is round.[(((((triple2) -> rule1)) -> rule5))] @3: Fiona is big.[(((((((triple2) -> rule1)) -> rule5)) -> rule8))] Fiona is blue.[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule5)) -> rule2))]
Erin is not nice.
("Erin" "is" "nice" "-")
triple1
Fiona is white.
("Fiona" "is" "white" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3