Anne is red. Gary is blue. Harry is kind. All red things are blue. All smart things are blue. If Harry is furry then Harry is smart. If Anne is not smart and Anne is not quiet then Anne is big. All kind things are furry. If something is furry and not quiet then it is red.
Anne is red.
("Anne" "is" "red" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If Harry is furry then Harry is smart.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "smart" "+"))
If Anne is not smart and Anne is not quiet then Anne is big.
((("Anne" "is" "smart" "~") ("Anne" "is" "quiet" "~")) -> ("Anne" "is" "big" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If something is furry and not quiet then it is red.
((("something" "is" "furry" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "red" "+"))
Harry is kind.
True
1
proof
[(triple3)]
("Harry" "is" "kind" "+")
triple3
Gary is not blue.
False
1
inv-proof
[(triple2)]
("Gary" "is" "blue" "-")
triple2
Harry is furry.
True
2
proof
[(((triple3) -> rule5))]
("Harry" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Harry is smart.
True
3
proof
[(((((triple3) -> rule5)) -> rule3))]
("Harry" "is" "smart" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule3))]
("Harry" "is" "smart" "-")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
True
4
proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
("Harry" "is" "blue" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not blue.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
("Harry" "is" "blue" "-")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "furry" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "red" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "furry" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is red.[(triple1)] Gary is blue.[(triple2)] Harry is kind.[(triple3)] @1: Anne is blue.[(((triple1) -> rule1))] Harry is furry.[(((triple3) -> rule5))] @2: Harry is smart.[(((((triple3) -> rule5)) -> rule3))] @3: Harry is blue.[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3