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