Bob is blue. Bob is furry. Bob is nice. Bob is quiet. Bob is rough. Bob is smart. Bob is young. Charlie is not blue. Charlie is nice. Charlie is not rough. Charlie is young. Dave is blue. Dave is furry. Dave is nice. Dave is smart. If something is young and smart then it is quiet. If something is quiet and not furry then it is not rough. If something is quiet then it is rough. All smart, blue things are rough. If Dave is blue and Dave is not furry then Dave is not young. All furry things are blue. Quiet things are young. Rough things are young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If something is young and smart then it is quiet.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and not furry then it is not rough.
((("something" "is" "quiet" "+") ("something" "is" "furry" "~")) -> ("something" "is" "rough" "-"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All smart, blue things are rough.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Dave is blue and Dave is not furry then Dave is not young.
((("Dave" "is" "blue" "+") ("Dave" "is" "furry" "~")) -> ("Dave" "is" "young" "-"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Dave is furry.
True
1
proof
[(triple13)]
("Dave" "is" "furry" "+")
triple13
Bob is not smart.
False
1
inv-proof
[(triple6)]
("Bob" "is" "smart" "-")
triple6
Dave is rough.
True
3
proof
[(((triple15 triple12) -> rule4) OR ((triple15 ((triple13) -> rule6)) -> rule4))]
("Dave" "is" "rough" "+")
((triple15 triple12) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple15 ((triple13) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((triple15 triple12) -> rule4) OR ((triple15 ((triple13) -> rule6)) -> rule4))]
("Dave" "is" "rough" "-")
((triple15 triple12) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple15 ((triple13) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
True
4
proof
[(((((triple15 triple12) -> rule4)) -> rule8) OR ((((triple15 ((triple13) -> rule6)) -> rule4)) -> rule8))]
("Dave" "is" "young" "+")
((((triple15 triple12) -> (rule4 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple15 ((triple13) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not young.
False
4
inv-proof
[(((((triple15 triple12) -> rule4)) -> rule8) OR ((((triple15 ((triple13) -> rule6)) -> rule4)) -> rule8))]
("Dave" "is" "young" "-")
((((triple15 triple12) -> (rule4 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple15 ((triple13) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is quiet.
True
6
proof
[(((((((triple15 triple12) -> rule4)) -> rule8) triple15) -> rule1) OR ((((((triple15 ((triple13) -> rule6)) -> rule4)) -> rule8) triple15) -> rule1))]
("Dave" "is" "quiet" "+")
((((((triple15 triple12) -> (rule4 % int3))) -> (rule8 % int2)) triple15) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple15 ((triple13) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple15) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not quiet.
False
6
inv-proof
[(((((((triple15 triple12) -> rule4)) -> rule8) triple15) -> rule1) OR ((((((triple15 ((triple13) -> rule6)) -> rule4)) -> rule8) triple15) -> rule1))]
("Dave" "is" "quiet" "-")
((((((triple15 triple12) -> (rule4 % int3))) -> (rule8 % int2)) triple15) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple15 ((triple13) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple15) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is blue.[(triple1 OR ((triple2) -> rule6))] Bob is furry.[(triple2)] Bob is nice.[(triple3)] Bob is quiet.[(triple4 OR ((triple7 triple6) -> rule1) OR ((((triple5) -> rule8) triple6) -> rule1) OR ((((((triple6 triple1) -> rule4)) -> rule8) triple6) -> rule1) OR ((((((triple6 ((triple2) -> rule6)) -> rule4)) -> rule8) triple6) -> rule1))] Bob is rough.[(triple5 OR ((triple4) -> rule3) OR ((triple6 triple1) -> rule4) OR ((((triple7 triple6) -> rule1)) -> rule3) OR ((triple6 ((triple2) -> rule6)) -> rule4))] Bob is smart.[(triple6)] Bob is young.[(triple7 OR ((triple4) -> rule7) OR ((triple5) -> rule8) OR ((((triple4) -> rule3)) -> rule8) OR ((((triple6 triple1) -> rule4)) -> rule8) OR ((((triple6 ((triple2) -> rule6)) -> rule4)) -> rule8))] Charlie is nice.[(triple9)] Charlie is not blue.[(triple8)] Charlie is not rough.[(triple10)] Charlie is young.[(triple11)] Dave is blue.[(triple12 OR ((triple13) -> rule6))] Dave is furry.[(triple13)] Dave is nice.[(triple14)] Dave is smart.[(triple15)] @1: Dave is rough.[(((triple15 triple12) -> rule4) OR ((triple15 ((triple13) -> rule6)) -> rule4))] @2: Dave is young.[(((((triple15 triple12) -> rule4)) -> rule8) OR ((((triple15 ((triple13) -> rule6)) -> rule4)) -> rule8))] @3: Dave is quiet.[(((((((triple15 triple12) -> rule4)) -> rule8) triple15) -> rule1) OR ((((((triple15 ((triple13) -> rule6)) -> rule4)) -> rule8) triple15) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple7 triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple5) -> (rule8 % int2)) triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((((triple6 triple1) -> (rule4 % int3))) -> (rule8 % int2)) triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((triple6 ((triple2) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple4) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple6 triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple7 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((triple6 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple4) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple5) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple6 triple1) -> (rule4 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple6 ((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple8
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple10
Charlie is young.
("Charlie" "is" "young" "+")
triple11
Dave is blue.
("Dave" "is" "blue" "+")
triple12
((triple13) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple13
Dave is nice.
("Dave" "is" "nice" "+")
triple14
Dave is smart.
("Dave" "is" "smart" "+")
triple15
Dave is rough.
("Dave" "is" "rough" "+")
((triple15 triple12) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple15 ((triple13) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple15 triple12) -> (rule4 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple15 ((triple13) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple15 triple12) -> (rule4 % int3))) -> (rule8 % int2)) triple15) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple15 ((triple13) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple15) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4