Erin is not nice. Fiona is nice. Gary is big. Harry is cold. If Fiona is furry then Fiona is not quiet. If something is cold then it is not kind. All furry things are quiet. If something is big and quiet then it is cold. If Gary is red then Gary is not quiet. If something is cold and not nice then it is furry. Big things are furry. Nice, big things are red.
Erin is not nice.
("Erin" "is" "nice" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Fiona is furry then Fiona is not quiet.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "quiet" "-"))
If something is cold then it is not kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "-"))
All furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is big and quiet then it is cold.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Gary is red then Gary is not quiet.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "quiet" "-"))
If something is cold and not nice then it is furry.
((("something" "is" "cold" "+") ("something" "is" "nice" "~")) -> ("something" "is" "furry" "+"))
Big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Nice, big things are red.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Fiona is nice.
True
1
proof
[(triple2)]
("Fiona" "is" "nice" "+")
triple2
Gary is not big.
False
1
inv-proof
[(triple3)]
("Gary" "is" "big" "-")
triple3
Harry is not kind.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "kind" "-")
((triple4) -> (rule2 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is kind.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Gary is quiet.
True
3
proof
[(((((triple3) -> rule7)) -> rule3))]
("Gary" "is" "quiet" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3))]
("Gary" "is" "quiet" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is cold.
True
5
proof
[(((triple3 ((((triple3) -> rule7)) -> rule3)) -> rule4))]
("Gary" "is" "cold" "+")
((triple3 ((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not cold.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule7)) -> rule3)) -> rule4))]
("Gary" "is" "cold" "-")
((triple3 ((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "furry" "-")
Fiona is quiet.
Unknown
rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "cold" "-")
Erin is quiet.
Unknown
rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Erin" "is" "quiet" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Erin is not nice.[(triple1)] Fiona is nice.[(triple2)] Gary is big.[(triple3)] Harry is cold.[(triple4)] @1: Gary is furry.[(((triple3) -> rule7))] Harry is not kind.[(((triple4) -> rule2))] @2: Gary is quiet.[(((((triple3) -> rule7)) -> rule3))] @3: Gary is cold.[(((triple3 ((((triple3) -> rule7)) -> rule3)) -> rule4))] @4: Gary is not kind.[(((((triple3 ((((triple3) -> rule7)) -> rule3)) -> rule4)) -> rule2))]
Erin is not nice.
("Erin" "is" "nice" "-")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
((triple3) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
((triple4) -> (rule2 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple3 ((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not kind.
("Gary" "is" "kind" "-")
((((triple3 ((((triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4