Bob is smart. Bob is white. Bob is not young. Dave is not red. Dave is not round. Dave is smart. Dave is white. Erin is furry. Erin is not nice. Erin is round. Erin is not smart. Erin is white. Harry is furry. Harry is not nice. Harry is not smart. If Harry is white and Harry is round then Harry is not young. Smart, red people are furry. All furry people are round. Young people are not round. If Dave is furry and Dave is not red then Dave is smart. If Bob is smart then Bob is red.
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is not young.
("Bob" "is" "young" "-")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not round.
("Dave" "is" "round" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is white.
("Erin" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is not smart.
("Harry" "is" "smart" "-")
If Harry is white and Harry is round then Harry is not young.
((("Harry" "is" "white" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "young" "-"))
Smart, red people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Young people are not round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "-"))
If Dave is furry and Dave is not red then Dave is smart.
((("Dave" "is" "furry" "+") ("Dave" "is" "red" "~")) -> ("Dave" "is" "smart" "+"))
If Bob is smart then Bob is red.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "red" "+"))
Erin is not smart.
True
1
proof
[(triple11)]
("Erin" "is" "smart" "-")
triple11
Erin is nice.
False
1
inv-proof
[(triple9)]
("Erin" "is" "nice" "+")
triple9
Harry is round.
True
2
proof
[(((triple13) -> rule3))]
("Harry" "is" "round" "+")
((triple13) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "red" "-")
((triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
True
4
proof
[(((triple1 ((triple1) -> rule6)) -> rule2))]
("Bob" "is" "furry" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not furry.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule2))]
("Bob" "is" "furry" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
True
5
proof
[(((((triple1 ((triple1) -> rule6)) -> rule2)) -> rule3))]
("Bob" "is" "round" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not round.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule6)) -> rule2)) -> rule3))]
("Bob" "is" "round" "-")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Bob is not young.[(triple3)] Bob is smart.[(triple1)] Bob is white.[(triple2)] Dave is not red.[(triple4)] Dave is not round.[(triple5)] Dave is smart.[(triple6)] Dave is white.[(triple7)] Erin is furry.[(triple8)] Erin is not nice.[(triple9)] Erin is not smart.[(triple11)] Erin is round.[(triple10 OR ((triple8) -> rule3))] Erin is white.[(triple12)] Harry is furry.[(triple13)] Harry is not nice.[(triple14)] Harry is not smart.[(triple15)] @1: Bob is red.[(((triple1) -> rule6))] Harry is round.[(((triple13) -> rule3))] @2: Bob is furry.[(((triple1 ((triple1) -> rule6)) -> rule2))] @3: Bob is round.[(((((triple1 ((triple1) -> rule6)) -> rule2)) -> rule3))]
Bob is not young.
("Bob" "is" "young" "-")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Dave is not red.
("Dave" "is" "red" "-")
triple4
Dave is not round.
("Dave" "is" "round" "-")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is not nice.
("Erin" "is" "nice" "-")
triple9
Erin is not smart.
("Erin" "is" "smart" "-")
triple11
Erin is round.
("Erin" "is" "round" "+")
triple10
((triple8) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is not nice.
("Harry" "is" "nice" "-")
triple14
Harry is not smart.
("Harry" "is" "smart" "-")
triple15
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple13) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3