Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is nice. Anne is round. Anne is young. Bob is big. Bob is blue. Bob is furry. If someone is blue then they are nice. Nice people are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Anne is young.
True
1
proof
[(triple7)]
("Anne" "is" "young" "+")
triple7
Anne is not furry.
False
1
inv-proof
[(triple4)]
("Anne" "is" "furry" "-")
triple4
Bob is nice.
True
2
proof
[(((triple9) -> rule1))]
("Bob" "is" "nice" "+")
((triple9) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple9) -> rule1))]
("Bob" "is" "nice" "-")
((triple9) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("Bob" "is" "round" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule2))]
("Bob" "is" "round" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is cold.[(triple3)] Anne is furry.[(triple4)] Anne is nice.[(triple5 OR ((triple2) -> rule1))] Anne is round.[(triple6 OR ((triple5) -> rule2) OR ((((triple2) -> rule1)) -> rule2))] Anne is young.[(triple7)] Bob is big.[(triple8)] Bob is blue.[(triple9)] Bob is furry.[(triple10)] @1: Bob is nice.[(((triple9) -> rule1))] @2: Bob is round.[(((((triple9) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
((triple2) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple5) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7
Bob is big.
("Bob" "is" "big" "+")
triple8
Bob is blue.
("Bob" "is" "blue" "+")
triple9
Bob is furry.
("Bob" "is" "furry" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple9) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2