Anne is cold. Bob is red. Dave is kind. Harry is nice. All kind people are cold. All big people are young. If someone is big then they are young. Cold people are big. If Dave is nice and Dave is not cold then Dave is furry. If Dave is not cold then Dave is red.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If Dave is nice and Dave is not cold then Dave is furry.
((("Dave" "is" "nice" "+") ("Dave" "is" "cold" "~")) -> ("Dave" "is" "furry" "+"))
If Dave is not cold then Dave is red.
((("Dave" "is" "cold" "~")) -> ("Dave" "is" "red" "+"))
Harry is nice.
True
1
proof
[(triple4)]
("Harry" "is" "nice" "+")
triple4
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is big.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "cold" "-")
((triple3) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("Dave" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2) OR ((((triple1) -> rule4)) -> rule3))]
("Anne" "is" "young" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is young.
True
4
proof
[(((((((triple3) -> rule1)) -> rule4)) -> rule2) OR ((((((triple3) -> rule1)) -> rule4)) -> rule3))]
("Dave" "is" "young" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not young.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule4)) -> rule2) OR ((((((triple3) -> rule1)) -> rule4)) -> rule3))]
("Dave" "is" "young" "-")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is young.
Unknown
rconc
[@3: Harry is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule1 <- FAIL)]]
("Harry" "is" "young" "+")
Bob is not big.
Unknown
inv-rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "red" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is cold.[(triple1)] Bob is red.[(triple2)] Dave is kind.[(triple3)] Harry is nice.[(triple4)] @1: Anne is big.[(((triple1) -> rule4))] Dave is cold.[(((triple3) -> rule1))] @2: Anne is young.[(((((triple1) -> rule4)) -> rule2) OR ((((triple1) -> rule4)) -> rule3))] Dave is big.[(((((triple3) -> rule1)) -> rule4))] @3: Dave is young.[(((((((triple3) -> rule1)) -> rule4)) -> rule2) OR ((((((triple3) -> rule1)) -> rule4)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3