Charlie is green. Charlie is young. Erin is furry. Erin is green. Erin is quiet. Erin is rough. Erin is round. Erin is white. Erin is young. Harry is furry. Harry is green. Harry is rough. Harry is round. Harry is white. Harry is young. Rough things are furry. If Erin is young then Erin is furry. All round things are green. If something is young and quiet then it is green. All green, white things are quiet. If Charlie is furry and Charlie is white then Charlie is rough. All white things are round. All young, white things are quiet.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If Erin is young then Erin is furry.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "furry" "+"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is young and quiet then it is green.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
All green, white things are quiet.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is furry and Charlie is white then Charlie is rough.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "rough" "+"))
All white things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All young, white things are quiet.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Harry is rough.
True
1
proof
[(triple12)]
("Harry" "is" "rough" "+")
triple12
Harry is not round.
False
1
inv-proof
[(triple13 OR ((triple14) -> rule7))]
("Harry" "is" "round" "-")
triple13
((triple14) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is green.[(triple1)] Charlie is young.[(triple2)] Erin is furry.[(triple3 OR ((triple6) -> rule1) OR ((triple9) -> rule2))] Erin is green.[(triple4 OR ((triple7) -> rule3) OR ((triple9 triple5) -> rule4) OR ((((triple8) -> rule7)) -> rule3) OR ((triple9 ((triple9 triple8) -> rule8)) -> rule4))] Erin is quiet.[(triple5 OR ((triple4 triple8) -> rule5) OR ((triple9 triple8) -> rule8) OR ((((triple7) -> rule3) triple8) -> rule5) OR ((((((triple8) -> rule7)) -> rule3) triple8) -> rule5))] Erin is rough.[(triple6)] Erin is round.[(triple7 OR ((triple8) -> rule7))] Erin is white.[(triple8)] Erin is young.[(triple9)] Harry is furry.[(triple10 OR ((triple12) -> rule1))] Harry is green.[(triple11 OR ((triple13) -> rule3) OR ((((triple14) -> rule7)) -> rule3) OR ((triple15 ((triple15 triple14) -> rule8)) -> rule4))] Harry is rough.[(triple12)] Harry is round.[(triple13 OR ((triple14) -> rule7))] Harry is white.[(triple14)] Harry is young.[(triple15)] @1: Harry is quiet.[(((triple11 triple14) -> rule5) OR ((triple15 triple14) -> rule8) OR ((((triple13) -> rule3) triple14) -> rule5) OR ((((((triple14) -> rule7)) -> rule3) triple14) -> rule5))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
((triple6) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple9) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple4
((triple7) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple9 triple5) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple8) -> (rule7 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((triple9 ((triple9 triple8) -> (rule8 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple4 triple8) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple9 triple8) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple7) -> (rule3 % int2)) triple8) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple8) -> (rule7 % int3))) -> (rule3 % int2)) triple8) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
((triple8) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
((triple12) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple11
((triple13) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple14) -> (rule7 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple15 ((triple15 triple14) -> (rule8 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
((triple14) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple11 triple14) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple15 triple14) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple13) -> (rule3 % int2)) triple14) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple14) -> (rule7 % int3))) -> (rule3 % int2)) triple14) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3