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