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