Bob is green. Bob is kind. Bob is quiet. Bob is not rough. Bob is round. Dave is big. Dave is blue. Dave is green. Dave is kind. Dave is quiet. Dave is rough. Dave is round. Harry is big. Harry is kind. Harry is rough. Harry is round. Quiet, round people are blue. If someone is round then they are quiet. If Bob is big then Bob is not rough.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Quiet, round people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is big then Bob is not rough.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "rough" "-"))
Harry is round.
True
1
proof
[(triple16)]
("Harry" "is" "round" "+")
triple16
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple16) -> rule2))]
("Harry" "is" "quiet" "+")
((triple16) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is not blue.
False
3
inv-proof
[(((triple3 triple5) -> rule1) OR ((((triple5) -> rule2) triple5) -> rule1))]
("Bob" "is" "blue" "-")
((triple3 triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple5) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Harry is blue.
True
4
proof
[(((((triple16) -> rule2) triple16) -> rule1))]
("Harry" "is" "blue" "+")
((((triple16) -> (rule2 % int2)) triple16) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((((triple16) -> rule2) triple16) -> rule1))]
("Harry" "is" "blue" "-")
((((triple16) -> (rule2 % int2)) triple16) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Bob is not rough.[(triple4)] Bob is quiet.[(triple3 OR ((triple5) -> rule2))] Bob is round.[(triple5)] Dave is big.[(triple6)] Dave is blue.[(triple7 OR ((triple10 triple12) -> rule1) OR ((((triple12) -> rule2) triple12) -> rule1))] Dave is green.[(triple8)] Dave is kind.[(triple9)] Dave is quiet.[(triple10 OR ((triple12) -> rule2))] Dave is rough.[(triple11)] Dave is round.[(triple12)] Harry is big.[(triple13)] Harry is kind.[(triple14)] Harry is rough.[(triple15)] Harry is round.[(triple16)] @1: Bob is blue.[(((triple3 triple5) -> rule1) OR ((((triple5) -> rule2) triple5) -> rule1))] Harry is quiet.[(((triple16) -> rule2))] @2: Harry is blue.[(((((triple16) -> rule2) triple16) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not rough.
("Bob" "is" "rough" "-")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple5) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
((triple10 triple12) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple12) -> (rule2 % int2)) triple12) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
((triple12) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple11
Dave is round.
("Dave" "is" "round" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16
Bob is blue.
("Bob" "is" "blue" "+")
((triple3 triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple5) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple16) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple16) -> (rule2 % int2)) triple16) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2