Bob is cold. Bob is young. Dave is cold. Dave is furry. Dave is quiet. Dave is round. Dave is white. Dave is young. Erin is furry. Erin is rough. Erin is round. Erin is young. All rough people are round. All furry people are white. If someone is white then they are young. All furry people are quiet. If someone is cold then they are rough. All rough, cold people are quiet. All furry people are white. If Erin is white then Erin is young.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
All rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
All furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold then they are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
All rough, cold people are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If Erin is white then Erin is young.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "young" "+"))
Dave is furry.
True
1
proof
[(triple4)]
("Dave" "is" "furry" "+")
triple4
Dave is not cold.
False
1
inv-proof
[(triple3)]
("Dave" "is" "cold" "-")
triple3
Dave is rough.
True
2
proof
[(((triple3) -> rule5))]
("Dave" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple9) -> rule2) OR ((triple9) -> rule7))]
("Erin" "is" "white" "-")
((triple9) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple9) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is quiet.
True
4
proof
[(((((triple1) -> rule5) triple1) -> rule6))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("Bob" "is" "round" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is cold.[(triple1)] Bob is young.[(triple2)] Dave is cold.[(triple3)] Dave is furry.[(triple4)] Dave is quiet.[(triple5 OR ((triple4) -> rule4) OR ((((triple3) -> rule5) triple3) -> rule6))] Dave is round.[(triple6 OR ((((triple3) -> rule5)) -> rule1))] Dave is white.[(triple7 OR ((triple4) -> rule2) OR ((triple4) -> rule7))] Dave is young.[(triple8 OR ((triple7) -> rule3) OR ((((triple4) -> rule2)) -> rule3) OR ((((triple4) -> rule7)) -> rule3))] Erin is furry.[(triple9)] Erin is rough.[(triple10)] Erin is round.[(triple11 OR ((triple10) -> rule1))] Erin is young.[(triple12 OR ((((triple9) -> rule2)) -> rule3) OR ((((triple9) -> rule2)) -> rule8) OR ((((triple9) -> rule7)) -> rule3) OR ((((triple9) -> rule7)) -> rule8))] @1: Bob is rough.[(((triple1) -> rule5))] Dave is rough.[(((triple3) -> rule5))] Erin is quiet.[(((triple9) -> rule4))] Erin is white.[(((triple9) -> rule2) OR ((triple9) -> rule7))] @2: Bob is quiet.[(((((triple1) -> rule5) triple1) -> rule6))] Bob is round.[(((((triple1) -> rule5)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((triple4) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple3) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple6
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple7
((triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple4) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple8
((triple7) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
((triple10) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple12
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple9) -> (rule7 % int2))) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple9) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple9) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple9) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2