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