Anne is big. Anne is cold. Anne is kind. Anne is nice. Anne is red. Anne is white. Bob is cold. Bob is not kind. Bob is red. Bob is white. Dave is not big. Dave is cold. Dave is red. Harry is big. Harry is furry. All furry things are nice. All big, kind things are nice. Nice things are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All big, kind things are nice.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Anne is white.
True
1
proof
[(triple6 OR ((triple4) -> rule3) OR ((((triple1 triple3) -> rule2)) -> rule3))]
("Anne" "is" "white" "+")
triple6
((triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple1 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Bob is kind.
False
1
inv-proof
[(triple8)]
("Bob" "is" "kind" "+")
triple8
Harry is nice.
True
2
proof
[(((triple15) -> rule1))]
("Harry" "is" "nice" "+")
((triple15) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple15) -> rule1))]
("Harry" "is" "nice" "-")
((triple15) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
True
3
proof
[(((((triple15) -> rule1)) -> rule3))]
("Harry" "is" "white" "+")
((((triple15) -> (rule1 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not white.
False
3
inv-proof
[(((((triple15) -> rule1)) -> rule3))]
("Harry" "is" "white" "-")
((((triple15) -> (rule1 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is nice.[(triple4 OR ((triple1 triple3) -> rule2))] Anne is red.[(triple5)] Anne is white.[(triple6 OR ((triple4) -> rule3) OR ((((triple1 triple3) -> rule2)) -> rule3))] Bob is cold.[(triple7)] Bob is not kind.[(triple8)] Bob is red.[(triple9)] Bob is white.[(triple10)] Dave is cold.[(triple12)] Dave is not big.[(triple11)] Dave is red.[(triple13)] Harry is big.[(triple14)] Harry is furry.[(triple15)] @1: Harry is nice.[(((triple15) -> rule1))] @2: Harry is white.[(((((triple15) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple1 triple3) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple1 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple7
Bob is not kind.
("Bob" "is" "kind" "-")
triple8
Bob is red.
("Bob" "is" "red" "+")
triple9
Bob is white.
("Bob" "is" "white" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
triple12
Dave is not big.
("Dave" "is" "big" "-")
triple11
Dave is red.
("Dave" "is" "red" "+")
triple13
Harry is big.
("Harry" "is" "big" "+")
triple14
Harry is furry.
("Harry" "is" "furry" "+")
triple15
Harry is nice.
("Harry" "is" "nice" "+")
((triple15) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple15) -> (rule1 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2