Bob is kind. Bob is nice. Bob is quiet. Bob is smart. Bob is white. Dave is green. Dave is nice. Fiona is furry. Fiona is green. Fiona is kind. Fiona is nice. Fiona is quiet. If someone is green then they are kind. All smart people are white. All nice, kind people are smart.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All nice, kind people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Bob is smart.
True
1
proof
[(triple4 OR ((triple2 triple1) -> rule3))]
("Bob" "is" "smart" "+")
triple4
((triple2 triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Fiona is not furry.
False
1
inv-proof
[(triple8)]
("Fiona" "is" "furry" "-")
triple8
Dave is kind.
True
2
proof
[(((triple6) -> rule1))]
("Dave" "is" "kind" "+")
((triple6) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is not smart.
False
3
inv-proof
[(((triple11 triple10) -> rule3) OR ((triple11 ((triple9) -> rule1)) -> rule3))]
("Fiona" "is" "smart" "-")
((triple11 triple10) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple11 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Dave is smart.
True
4
proof
[(((triple7 ((triple6) -> rule1)) -> rule3))]
("Dave" "is" "smart" "+")
((triple7 ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Fiona is not white.
False
4
inv-proof
[(((((triple11 triple10) -> rule3)) -> rule2) OR ((((triple11 ((triple9) -> rule1)) -> rule3)) -> rule2))]
("Fiona" "is" "white" "-")
((((triple11 triple10) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple11 ((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3)] Bob is smart.[(triple4 OR ((triple2 triple1) -> rule3))] Bob is white.[(triple5 OR ((triple4) -> rule2) OR ((((triple2 triple1) -> rule3)) -> rule2))] Dave is green.[(triple6)] Dave is nice.[(triple7)] Fiona is furry.[(triple8)] Fiona is green.[(triple9)] Fiona is kind.[(triple10 OR ((triple9) -> rule1))] Fiona is nice.[(triple11)] Fiona is quiet.[(triple12)] @1: Dave is kind.[(((triple6) -> rule1))] Fiona is smart.[(((triple11 triple10) -> rule3) OR ((triple11 ((triple9) -> rule1)) -> rule3))] @2: Dave is smart.[(((triple7 ((triple6) -> rule1)) -> rule3))] Fiona is white.[(((((triple11 triple10) -> rule3)) -> rule2) OR ((((triple11 ((triple9) -> rule1)) -> rule3)) -> rule2))] @3: Dave is white.[(((((triple7 ((triple6) -> rule1)) -> rule3)) -> rule2))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((triple2 triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple5
((triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
((triple9) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple12
Dave is kind.
("Dave" "is" "kind" "+")
((triple6) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple11 triple10) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple11 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple7 ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple11 triple10) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple11 ((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((triple7 ((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3