Bob is blue. Bob is kind. Bob is smart. Bob is young. Dave is not big. Dave is blue. Dave is not kind. Dave is nice. Dave is young. Harry is not big. Harry is not blue. Harry is kind. Harry is nice. Harry is not red. Harry is smart. Harry is not young. If Bob is smart and Bob is young then Bob is kind. If Bob is big and Bob is smart then Bob is kind. If someone is young and not big then they are smart. Young, smart people are red. If someone is blue and not nice then they are not red. All big people are young. If Dave is smart and Dave is blue then Dave is red. If Dave is not young then Dave is red.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is not young.
("Harry" "is" "young" "-")
If Bob is smart and Bob is young then Bob is kind.
((("Bob" "is" "smart" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "kind" "+"))
If Bob is big and Bob is smart then Bob is kind.
((("Bob" "is" "big" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "kind" "+"))
If someone is young and not big then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "smart" "+"))
Young, smart people are red.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and not nice then they are not red.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "red" "-"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If Dave is smart and Dave is blue then Dave is red.
((("Dave" "is" "smart" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "red" "+"))
If Dave is not young then Dave is red.
((("Dave" "is" "young" "~")) -> ("Dave" "is" "red" "+"))
Dave is young.
True
1
proof
[(triple9)]
("Dave" "is" "young" "+")
triple9
Harry is not smart.
False
1
inv-proof
[(triple15)]
("Harry" "is" "smart" "-")
triple15
Dave is smart.
True
3
proof
[(((triple9 triple5) -> rule3))]
("Dave" "is" "smart" "+")
((triple9 triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
3
inv-proof
[(((triple9 triple5) -> rule3))]
("Dave" "is" "smart" "-")
((triple9 triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
True
5
proof
[(((triple9 ((triple9 triple5) -> rule3)) -> rule4) OR ((((triple9 triple5) -> rule3) triple6) -> rule7))]
("Dave" "is" "red" "+")
((triple9 ((triple9 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple9 triple5) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not red.
False
5
inv-proof
[(((triple9 ((triple9 triple5) -> rule3)) -> rule4) OR ((((triple9 triple5) -> rule3) triple6) -> rule7))]
("Dave" "is" "red" "-")
((triple9 ((triple9 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple9 triple5) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Bob is kind.[(triple2 OR ((triple3 triple4) -> rule1))] Bob is smart.[(triple3)] Bob is young.[(triple4)] Dave is blue.[(triple6)] Dave is nice.[(triple8)] Dave is not big.[(triple5)] Dave is not kind.[(triple7)] Dave is young.[(triple9)] Harry is kind.[(triple12)] Harry is nice.[(triple13)] Harry is not big.[(triple10)] Harry is not blue.[(triple11)] Harry is not red.[(triple14)] Harry is not young.[(triple16)] Harry is smart.[(triple15)] @1: Bob is red.[(((triple4 triple3) -> rule4))] Dave is smart.[(((triple9 triple5) -> rule3))] @2: Dave is red.[(((triple9 ((triple9 triple5) -> rule3)) -> rule4) OR ((((triple9 triple5) -> rule3) triple6) -> rule7))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((triple3 triple4) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Dave is not big.
("Dave" "is" "big" "-")
triple5
Dave is not kind.
("Dave" "is" "kind" "-")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is not big.
("Harry" "is" "big" "-")
triple10
Harry is not blue.
("Harry" "is" "blue" "-")
triple11
Harry is not red.
("Harry" "is" "red" "-")
triple14
Harry is not young.
("Harry" "is" "young" "-")
triple16
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Bob is red.
("Bob" "is" "red" "+")
((triple4 triple3) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple9 triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple9 ((triple9 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple9 triple5) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2