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