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