Bob is green. Bob is quiet. Bob is rough. Bob is white. Dave is kind. Dave is nice. Dave is rough. Erin is green. Erin is kind. Erin is smart. Erin is white. Harry is green. Harry is kind. Harry is nice. Harry is rough. Harry is white. Smart, rough things are nice. If Bob is green and Bob is white then Bob is smart. If something is rough then it is green.
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Smart, rough things are nice.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If Bob is green and Bob is white then Bob is smart.
((("Bob" "is" "green" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "smart" "+"))
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Harry is green.
True
1
proof
[(triple12 OR ((triple15) -> rule3))]
("Harry" "is" "green" "+")
triple12
((triple15) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Erin is not smart.
False
1
inv-proof
[(triple10)]
("Erin" "is" "smart" "-")
triple10
Bob is smart.
True
3
proof
[(((triple1 triple4) -> rule2) OR ((((triple3) -> rule3) triple4) -> rule2))]
("Bob" "is" "smart" "+")
((triple1 triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((triple1 triple4) -> rule2) OR ((((triple3) -> rule3) triple4) -> rule2))]
("Bob" "is" "smart" "-")
((triple1 triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is nice.
True
5
proof
[(((((triple1 triple4) -> rule2) triple3) -> rule1) OR ((((((triple3) -> rule3) triple4) -> rule2) triple3) -> rule1))]
("Bob" "is" "nice" "+")
((((triple1 triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple3) -> (rule3 % int3)) triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not nice.
False
5
inv-proof
[(((((triple1 triple4) -> rule2) triple3) -> rule1) OR ((((((triple3) -> rule3) triple4) -> rule2) triple3) -> rule1))]
("Bob" "is" "nice" "-")
((((triple1 triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple3) -> (rule3 % int3)) triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "nice" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Bob is green.[(triple1 OR ((triple3) -> rule3))] Bob is quiet.[(triple2)] Bob is rough.[(triple3)] Bob is white.[(triple4)] Dave is kind.[(triple5)] Dave is nice.[(triple6)] Dave is rough.[(triple7)] Erin is green.[(triple8)] Erin is kind.[(triple9)] Erin is smart.[(triple10)] Erin is white.[(triple11)] Harry is green.[(triple12 OR ((triple15) -> rule3))] Harry is kind.[(triple13)] Harry is nice.[(triple14)] Harry is rough.[(triple15)] Harry is white.[(triple16)] @1: Bob is smart.[(((triple1 triple4) -> rule2) OR ((((triple3) -> rule3) triple4) -> rule2))] Dave is green.[(((triple7) -> rule3))] @2: Bob is nice.[(((((triple1 triple4) -> rule2) triple3) -> rule1) OR ((((((triple3) -> rule3) triple4) -> rule2) triple3) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
((triple3) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
((triple15) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Bob is smart.
("Bob" "is" "smart" "+")
((triple1 triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple7) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1 triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple3) -> (rule3 % int3)) triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3