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